Proof of Theorem ghmeqker
Step | Hyp | Ref
| Expression |
1 | | ghmeqker.k |
. . . . 5
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
2 | | ghmeqker.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑇) |
3 | 2 | sneqi 4595 |
. . . . . 6
⊢ { 0 } =
{(0g‘𝑇)} |
4 | 3 | imaeq2i 6009 |
. . . . 5
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ {(0g‘𝑇)}) |
5 | 1, 4 | eqtri 2764 |
. . . 4
⊢ 𝐾 = (◡𝐹 “ {(0g‘𝑇)}) |
6 | 5 | eleq2i 2829 |
. . 3
⊢ ((𝑈 − 𝑉) ∈ 𝐾 ↔ (𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)})) |
7 | | ghmeqker.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
8 | | eqid 2736 |
. . . . . . 7
⊢
(Base‘𝑇) =
(Base‘𝑇) |
9 | 7, 8 | ghmf 19003 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) |
10 | 9 | ffnd 6666 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn 𝐵) |
11 | 10 | 3ad2ant1 1133 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹 Fn 𝐵) |
12 | | fniniseg 7007 |
. . . 4
⊢ (𝐹 Fn 𝐵 → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
13 | 11, 12 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
14 | 6, 13 | bitrid 282 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ 𝐾 ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
15 | | ghmgrp1 19001 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
16 | | ghmeqker.m |
. . . . . 6
⊢ − =
(-g‘𝑆) |
17 | 7, 16 | grpsubcl 18818 |
. . . . 5
⊢ ((𝑆 ∈ Grp ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) |
18 | 15, 17 | syl3an1 1163 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) |
19 | 18 | biantrurd 533 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
20 | | eqid 2736 |
. . . . 5
⊢
(-g‘𝑇) = (-g‘𝑇) |
21 | 7, 16, 20 | ghmsub 19007 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉))) |
22 | 21 | eqeq1d 2738 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) |
23 | 19, 22 | bitr3d 280 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) |
24 | | ghmgrp2 19002 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
25 | 24 | 3ad2ant1 1133 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑇 ∈ Grp) |
26 | 9 | 3ad2ant1 1133 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹:𝐵⟶(Base‘𝑇)) |
27 | | simp2 1137 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑈 ∈ 𝐵) |
28 | 26, 27 | ffvelcdmd 7032 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑈) ∈ (Base‘𝑇)) |
29 | | simp3 1138 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑉 ∈ 𝐵) |
30 | 26, 29 | ffvelcdmd 7032 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑉) ∈ (Base‘𝑇)) |
31 | | eqid 2736 |
. . . 4
⊢
(0g‘𝑇) = (0g‘𝑇) |
32 | 8, 31, 20 | grpsubeq0 18824 |
. . 3
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇)) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) |
33 | 25, 28, 30, 32 | syl3anc 1371 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) |
34 | 14, 23, 33 | 3bitrrd 305 |
1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ (𝑈 − 𝑉) ∈ 𝐾)) |