Proof of Theorem ghmeqker
Step | Hyp | Ref
| Expression |
1 | | ghmeqker.k |
. . . . 5
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
2 | | ghmeqker.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑇) |
3 | 2 | sneqi 4188 |
. . . . . 6
⊢ { 0 } =
{(0g‘𝑇)} |
4 | 3 | imaeq2i 5464 |
. . . . 5
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ {(0g‘𝑇)}) |
5 | 1, 4 | eqtri 2644 |
. . . 4
⊢ 𝐾 = (◡𝐹 “ {(0g‘𝑇)}) |
6 | 5 | eleq2i 2693 |
. . 3
⊢ ((𝑈 − 𝑉) ∈ 𝐾 ↔ (𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)})) |
7 | | ghmeqker.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
8 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑇) =
(Base‘𝑇) |
9 | 7, 8 | ghmf 17664 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) |
10 | | ffn 6045 |
. . . . . 6
⊢ (𝐹:𝐵⟶(Base‘𝑇) → 𝐹 Fn 𝐵) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn 𝐵) |
12 | 11 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹 Fn 𝐵) |
13 | | fniniseg 6338 |
. . . 4
⊢ (𝐹 Fn 𝐵 → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
15 | 6, 14 | syl5bb 272 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ 𝐾 ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
16 | | ghmgrp1 17662 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
17 | | ghmeqker.m |
. . . . . 6
⊢ − =
(-g‘𝑆) |
18 | 7, 17 | grpsubcl 17495 |
. . . . 5
⊢ ((𝑆 ∈ Grp ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) |
19 | 16, 18 | syl3an1 1359 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) |
20 | 19 | biantrurd 529 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) |
21 | | eqid 2622 |
. . . . 5
⊢
(-g‘𝑇) = (-g‘𝑇) |
22 | 7, 17, 21 | ghmsub 17668 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉))) |
23 | 22 | eqeq1d 2624 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) |
24 | 20, 23 | bitr3d 270 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) |
25 | | ghmgrp2 17663 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
26 | 25 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑇 ∈ Grp) |
27 | 9 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹:𝐵⟶(Base‘𝑇)) |
28 | | simp2 1062 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑈 ∈ 𝐵) |
29 | 27, 28 | ffvelrnd 6360 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑈) ∈ (Base‘𝑇)) |
30 | | simp3 1063 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑉 ∈ 𝐵) |
31 | 27, 30 | ffvelrnd 6360 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑉) ∈ (Base‘𝑇)) |
32 | | eqid 2622 |
. . . 4
⊢
(0g‘𝑇) = (0g‘𝑇) |
33 | 8, 32, 21 | grpsubeq0 17501 |
. . 3
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇)) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) |
34 | 26, 29, 31, 33 | syl3anc 1326 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) |
35 | 15, 24, 34 | 3bitrrd 295 |
1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ (𝑈 − 𝑉) ∈ 𝐾)) |