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