This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ghm0to0

Description: 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)

Ref Expression
Hypotheses f1ghm0to0.a 
|- A = ( Base ` R )
f1ghm0to0.b 
|- B = ( Base ` S )
f1ghm0to0.n 
|- N = ( 0g ` R )
f1ghm0to0.0 
|- .0. = ( 0g ` S )
Assertion f1ghm0to0 
|- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = .0. <-> X = N ) )

Proof

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