Theorem gim0to0

Description: A group isomorphism 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, 23-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		gim0to0.a	|- A = ( Base ` R )
2		gim0to0.b	|- B = ( Base ` S )
3		gim0to0.n	|- N = ( 0g ` S )
4		gim0to0.0	|- .0. = ( 0g ` R )
5		gimghm	|- ( F e. ( R GrpIso S ) -> F e. ( R GrpHom S ) )
6	1 2	gimf1o	|- ( F e. ( R GrpIso S ) -> F : A -1-1-onto-> B )
7		f1of1	|- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
8	6 7	syl	|- ( F e. ( R GrpIso S ) -> F : A -1-1-> B )
9	5 8	jca	|- ( F e. ( R GrpIso S ) -> ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) )
10	9	anim1i	|- ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ X e. A ) )
11		df-3an	|- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) <-> ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ X e. A ) )
12	10 11	sylibr	|- ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) )
13	1 2 4 3	f1ghm0to0	|- ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )
14	12 13	syl	|- ( ( F e. ( R GrpIso S ) /\ X e. A ) -> ( ( F ` X ) = N <-> X = .0. ) )