f1ghm0to0.mmp

f1ghm0to0.mmp

$theorem f1ghm0to0

* If a group homomorphism ` F ` is injective, it maps the zero of one
       group (and only the zero) to the zero of the other group.  (Contributed
       by AV, 24-Oct-2019.)  (Revised by Thierry Arnoux, 13-May-2023.)

h1::f1ghm0to0.a          |- A = ( Base ` R )
h2::f1ghm0to0.b    |- B = ( Base ` S )
h3::f1ghm0to0.n         |- N = ( 0g ` S )
h4::f1ghm0to0.1          |- .0. = ( 0g ` R )
6:4,3:ghmid            |- ( F e. ( R GrpHom S ) -> ( F ` .0. ) = N )
8:6:3ad2ant1          |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( F ` .0. ) = N )
9:8:eqeq2d           |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = ( F ` .0. ) <-> ( F ` X ) = N ) )
10::simp2             |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> F : A -1-1-> B )
11::simp3             |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> X e. A )
12::ghmgrp1             |- ( F e. ( R GrpHom S ) -> R e. Grp )
13:1,4:grpidcl          |- ( R e. Grp -> .0. e. A )
14:12,13:syl           |- ( F e. ( R GrpHom S ) -> .0. e. A )
15:14:3ad2ant1        |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> .0. e. A )
16::f1veqaeq          |- ( ( F : A -1-1-> B /\ ( X e. A /\ .0. e. A ) ) -> ( ( F ` X ) = ( F ` .0. ) -> X = .0. ) )
17:10,11,15,16:syl12anc
                     |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = ( F ` .0. ) -> X = .0. ) )
18:9,17:sylbird     |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N -> X = .0. ) )
19::fveq2             |- ( X = .0. -> ( F ` X ) = ( F ` .0. ) )
20:19,8:sylan9eqr    |- ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) /\ X = .0. ) -> ( F ` X ) = N )
21:20:ex            |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( X = .0. -> ( F ` X ) = N ) )
qed:18,21:impbid   |- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )

$= ( cghm co wcel wf1 w3a cfv wceq ghmid 3ad2ant1 eqeq2d wi simp2 simp3 cgrp
   ghmgrp1 grpidcl syl f1veqaeq syl12anc sylbird fveq2 sylan9eqr ex impbid ) EC
   DMNZOZABEPZGAOZQZGERZFSZGHSZVAVCVBHERZSZVDVAVEFVBURUSVEFSZUTCDEHFLKTUAUBVAUS
   UTHAOZVFVDUCURUSUTUDURUSUTUEURUSVHUTURCUFOVHCDEUGACHILUHUIUAABGHEUJUKULVAVDV
   CVDVAVBVEFGHEUMURUSVGUTCDEHFLKTUAUNUOUP $.