Step | Hyp | Ref
| Expression |
1 | | ghmf1.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑆) |
2 | | ghmf1.u |
. . . . . . . 8
⊢ 𝑈 = (0g‘𝑇) |
3 | 1, 2 | ghmid 17489 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘ 0 ) = 𝑈) |
4 | 3 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → (𝐹‘ 0 ) = 𝑈) |
5 | 4 | eqeq2d 2620 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = (𝐹‘ 0 ) ↔ (𝐹‘𝑥) = 𝑈)) |
6 | | simplr 788 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋–1-1→𝑌) |
7 | | simpr 476 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
8 | | ghmgrp1 17485 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
9 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑆 ∈ Grp) |
10 | | ghmf1.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝑆) |
11 | 10, 1 | grpidcl 17273 |
. . . . . . 7
⊢ (𝑆 ∈ Grp → 0 ∈ 𝑋) |
12 | 9, 11 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → 0 ∈ 𝑋) |
13 | | f1fveq 6420 |
. . . . . 6
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ (𝑥 ∈ 𝑋 ∧ 0 ∈ 𝑋)) → ((𝐹‘𝑥) = (𝐹‘ 0 ) ↔ 𝑥 = 0 )) |
14 | 6, 7, 12, 13 | syl12anc 1316 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = (𝐹‘ 0 ) ↔ 𝑥 = 0 )) |
15 | 5, 14 | bitr3d 269 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 𝑈 ↔ 𝑥 = 0 )) |
16 | 15 | biimpd 218 |
. . 3
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) |
17 | 16 | ralrimiva 2949 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋–1-1→𝑌) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) |
18 | | ghmf1.y |
. . . . 5
⊢ 𝑌 = (Base‘𝑇) |
19 | 10, 18 | ghmf 17487 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌) |
20 | 19 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) → 𝐹:𝑋⟶𝑌) |
21 | | eqid 2610 |
. . . . . . . . . 10
⊢
(-g‘𝑆) = (-g‘𝑆) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢
(-g‘𝑇) = (-g‘𝑇) |
23 | 10, 21, 22 | ghmsub 17491 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝐹‘(𝑦(-g‘𝑆)𝑧)) = ((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧))) |
24 | 23 | 3expb 1258 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝐹‘(𝑦(-g‘𝑆)𝑧)) = ((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧))) |
25 | 24 | adantlr 747 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝐹‘(𝑦(-g‘𝑆)𝑧)) = ((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧))) |
26 | 25 | eqeq1d 2612 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝐹‘(𝑦(-g‘𝑆)𝑧)) = 𝑈 ↔ ((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧)) = 𝑈)) |
27 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) → 𝑆 ∈ Grp) |
28 | 10, 21 | grpsubcl 17318 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝑆)𝑧) ∈ 𝑋) |
29 | 28 | 3expb 1258 |
. . . . . . . 8
⊢ ((𝑆 ∈ Grp ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦(-g‘𝑆)𝑧) ∈ 𝑋) |
30 | 27, 29 | sylan 487 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦(-g‘𝑆)𝑧) ∈ 𝑋) |
31 | | simplr 788 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) |
32 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦(-g‘𝑆)𝑧) → (𝐹‘𝑥) = (𝐹‘(𝑦(-g‘𝑆)𝑧))) |
33 | 32 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦(-g‘𝑆)𝑧) → ((𝐹‘𝑥) = 𝑈 ↔ (𝐹‘(𝑦(-g‘𝑆)𝑧)) = 𝑈)) |
34 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦(-g‘𝑆)𝑧) → (𝑥 = 0 ↔ (𝑦(-g‘𝑆)𝑧) = 0 )) |
35 | 33, 34 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = (𝑦(-g‘𝑆)𝑧) → (((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 ) ↔ ((𝐹‘(𝑦(-g‘𝑆)𝑧)) = 𝑈 → (𝑦(-g‘𝑆)𝑧) = 0 ))) |
36 | 35 | rspcv 3278 |
. . . . . . 7
⊢ ((𝑦(-g‘𝑆)𝑧) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 ) → ((𝐹‘(𝑦(-g‘𝑆)𝑧)) = 𝑈 → (𝑦(-g‘𝑆)𝑧) = 0 ))) |
37 | 30, 31, 36 | sylc 63 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝐹‘(𝑦(-g‘𝑆)𝑧)) = 𝑈 → (𝑦(-g‘𝑆)𝑧) = 0 )) |
38 | 26, 37 | sylbird 249 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧)) = 𝑈 → (𝑦(-g‘𝑆)𝑧) = 0 )) |
39 | | ghmgrp2 17486 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
40 | 39 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑇 ∈ Grp) |
41 | 19 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝐹:𝑋⟶𝑌) |
42 | | simprl 790 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
43 | 41, 42 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝐹‘𝑦) ∈ 𝑌) |
44 | | simprr 792 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
45 | 41, 44 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝐹‘𝑧) ∈ 𝑌) |
46 | 18, 2, 22 | grpsubeq0 17324 |
. . . . . 6
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑦) ∈ 𝑌 ∧ (𝐹‘𝑧) ∈ 𝑌) → (((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧)) = 𝑈 ↔ (𝐹‘𝑦) = (𝐹‘𝑧))) |
47 | 40, 43, 45, 46 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (((𝐹‘𝑦)(-g‘𝑇)(𝐹‘𝑧)) = 𝑈 ↔ (𝐹‘𝑦) = (𝐹‘𝑧))) |
48 | 8 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑆 ∈ Grp) |
49 | 10, 1, 21 | grpsubeq0 17324 |
. . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑦(-g‘𝑆)𝑧) = 0 ↔ 𝑦 = 𝑧)) |
50 | 48, 42, 44, 49 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(-g‘𝑆)𝑧) = 0 ↔ 𝑦 = 𝑧)) |
51 | 38, 47, 50 | 3imtr3d 281 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
52 | 51 | ralrimivva 2954 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
53 | | dff13 6416 |
. . 3
⊢ (𝐹:𝑋–1-1→𝑌 ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
54 | 20, 52, 53 | sylanbrc 695 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 )) → 𝐹:𝑋–1-1→𝑌) |
55 | 17, 54 | impbida 873 |
1
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1→𝑌 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 ))) |