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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 gim0to0.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
2 gim0to0.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 gim0to0.n ⊢ 𝑁 = ( 0g ‘ 𝑆 )
4 gim0to0.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 4 3 f1ghm0to0 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )
14 12 13 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑁 ↔ 𝑋 = 0 ) )