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	gim0to0ALT.a	⊢ 𝐴 = ( Base ‘ 𝑅 )
	gim0to0ALT.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	gim0to0ALT.n	⊢ 𝑁 = ( 0g ‘ 𝑆 )
	gim0to0ALT.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	gim0to0	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		gim0to0ALT.a	⊢ 𝐴 = ( Base ‘ 𝑅 )
2		gim0to0ALT.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		gim0to0ALT.n	⊢ 𝑁 = ( 0g ‘ 𝑆 )
4		gim0to0ALT.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		gimghm	⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
6	1 2	gimf1o	⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
7		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
8	6 7	syl	⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
9	5 8	jca	⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
10	9	anim1i	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) )
11		df-3an	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ↔ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) )
12	10 11	sylibr	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) )
13	1 2 3 4	f1ghm0to0	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )
14	12 13	syl	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )