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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 f1ghm0to0.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
2 f1ghm0to0.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 f1ghm0to0.n ⊢ 𝑁 = ( 0g ‘ 𝑅 )
4 f1ghm0to0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
5 3 4 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 𝑁 ) = 0 )
6 5 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑁 ) = 0 )
7 6 eqeq2d ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑁 ) ↔ ( 𝐹 ‘ 𝑋 ) = 0 ) )
8 simp2 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
9 simp3 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
10 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑅 ∈ Grp )
11 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 𝑁 ∈ 𝐴 )
12 10 11 syl ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑁 ∈ 𝐴 )
13 12 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑁 ∈ 𝐴 )
14 f1veqaeq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑁 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑁 ) → 𝑋 = 𝑁 ) )
15 8 9 13 14 syl12anc ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑁 ) → 𝑋 = 𝑁 ) )
16 7 15 sylbird ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 → 𝑋 = 𝑁 ) )
17 fveq2 ⊢ ( 𝑋 = 𝑁 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑁 ) )
18 17 6 sylan9eqr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 𝑁 ) → ( 𝐹 ‘ 𝑋 ) = 0 )
19 18 ex ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = 𝑁 → ( 𝐹 ‘ 𝑋 ) = 0 ) )
20 16 19 impbid ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 𝑁 ) )