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 ` S )
	f1ghm0to0.1	|- .0. = ( 0g ` R )
Assertion	f1ghm0to0	|- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )

Proof

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