Metamath Proof Explorer

Theorem ghmf1

Description: Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses ghmf1.x ⊢ 𝑋 = ( Base ‘ 𝑆 )
ghmf1.y ⊢ 𝑌 = ( Base ‘ 𝑇 )
ghmf1.z ⊢ 0 = ( 0g ‘ 𝑆 )
ghmf1.u ⊢ 𝑈 = ( 0g ‘ 𝑇 )
Assertion ghmf1 ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 ghmf1.x ⊢ 𝑋 = ( Base ‘ 𝑆 )
2 ghmf1.y ⊢ 𝑌 = ( Base ‘ 𝑇 )
3 ghmf1.z ⊢ 0 = ( 0g ‘ 𝑆 )
4 ghmf1.u ⊢ 𝑈 = ( 0g ‘ 𝑇 )
5 3 4 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 0 ) = 𝑈 )
6 5 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 0 ) = 𝑈 )
7 6 eqeq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) )
8 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
9 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
10 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
11 10 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ Grp )
12 1 3 grpidcl ⊢ ( 𝑆 ∈ Grp → 0 ∈ 𝑋 )
13 11 12 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ 𝑋 )
14 f1fveq ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) ↔ 𝑥 = 0 ) )
15 8 9 13 14 syl12anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) ↔ 𝑥 = 0 ) )
16 7 15 bitr3d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑈 ↔ 𝑥 = 0 ) )
17 16 biimpd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) )
18 17 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) )
19 1 2 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
20 19 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
21 eqid ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
22 eqid ⊢ ( -g ‘ 𝑇 ) = ( -g ‘ 𝑇 )
23 1 21 22 ghmsub ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) )
24 23 3expb ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) )
25 24 adantlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) )
26 25 eqeq1d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = 𝑈 ↔ ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) = 𝑈 ) )
27 fveqeq2 ⊢ ( 𝑥 = ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑈 ↔ ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = 𝑈 ) )
28 eqeq1 ⊢ ( 𝑥 = ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ) )
29 27 28 imbi12d ⊢ ( 𝑥 = ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ↔ ( ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = 𝑈 → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ) ) )
30 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) )
31 10 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) → 𝑆 ∈ Grp )
32 1 21 grpsubcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ∈ 𝑋 )
33 32 3expb ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ∈ 𝑋 )
34 31 33 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ∈ 𝑋 )
35 29 30 34 rspcdva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) ) = 𝑈 → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ) )
36 26 35 sylbird ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) = 𝑈 → ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ) )
37 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
38 37 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑇 ∈ Grp )
39 19 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
40 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
41 39 40 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
42 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
43 39 42 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 )
44 2 4 22 grpsubeq0 ⊢ ( ( 𝑇 ∈ Grp ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 ) → ( ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) = 𝑈 ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
45 38 41 43 44 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑧 ) ) = 𝑈 ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
46 10 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑆 ∈ Grp )
47 1 3 21 grpsubeq0 ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) )
48 46 40 42 47 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 ( -g ‘ 𝑆 ) 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) )
49 36 45 48 3imtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
50 49 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
51 dff13 ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
52 20 50 51 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
53 18 52 impbida ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 𝑈 → 𝑥 = 0 ) ) )