Proof of Theorem ghmeqker
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ghmeqker.k | . . . . 5
⊢ 𝐾 = (◡𝐹 “ { 0 }) | 
| 2 |  | ghmeqker.z | . . . . . . 7
⊢  0 =
(0g‘𝑇) | 
| 3 | 2 | sneqi 4637 | . . . . . 6
⊢ { 0 } =
{(0g‘𝑇)} | 
| 4 | 3 | imaeq2i 6076 | . . . . 5
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ {(0g‘𝑇)}) | 
| 5 | 1, 4 | eqtri 2765 | . . . 4
⊢ 𝐾 = (◡𝐹 “ {(0g‘𝑇)}) | 
| 6 | 5 | eleq2i 2833 | . . 3
⊢ ((𝑈 − 𝑉) ∈ 𝐾 ↔ (𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)})) | 
| 7 |  | ghmeqker.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑆) | 
| 8 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑇) =
(Base‘𝑇) | 
| 9 | 7, 8 | ghmf 19238 | . . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) | 
| 10 | 9 | ffnd 6737 | . . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 Fn 𝐵) | 
| 11 | 10 | 3ad2ant1 1134 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹 Fn 𝐵) | 
| 12 |  | fniniseg 7080 | . . . 4
⊢ (𝐹 Fn 𝐵 → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) | 
| 13 | 11, 12 | syl 17 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ (◡𝐹 “ {(0g‘𝑇)}) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) | 
| 14 | 6, 13 | bitrid 283 | . 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝑈 − 𝑉) ∈ 𝐾 ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) | 
| 15 |  | ghmgrp1 19236 | . . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) | 
| 16 |  | ghmeqker.m | . . . . . 6
⊢  − =
(-g‘𝑆) | 
| 17 | 7, 16 | grpsubcl 19038 | . . . . 5
⊢ ((𝑆 ∈ Grp ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) | 
| 18 | 15, 17 | syl3an1 1164 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) ∈ 𝐵) | 
| 19 | 18 | biantrurd 532 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)))) | 
| 20 |  | eqid 2737 | . . . . 5
⊢
(-g‘𝑇) = (-g‘𝑇) | 
| 21 | 7, 16, 20 | ghmsub 19242 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉))) | 
| 22 | 21 | eqeq1d 2739 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) | 
| 23 | 19, 22 | bitr3d 281 | . 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝑈 − 𝑉) ∈ 𝐵 ∧ (𝐹‘(𝑈 − 𝑉)) = (0g‘𝑇)) ↔ ((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇))) | 
| 24 |  | ghmgrp2 19237 | . . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) | 
| 25 | 24 | 3ad2ant1 1134 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑇 ∈ Grp) | 
| 26 | 9 | 3ad2ant1 1134 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝐹:𝐵⟶(Base‘𝑇)) | 
| 27 |  | simp2 1138 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑈 ∈ 𝐵) | 
| 28 | 26, 27 | ffvelcdmd 7105 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑈) ∈ (Base‘𝑇)) | 
| 29 |  | simp3 1139 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑉 ∈ 𝐵) | 
| 30 | 26, 29 | ffvelcdmd 7105 | . . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑉) ∈ (Base‘𝑇)) | 
| 31 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑇) = (0g‘𝑇) | 
| 32 | 8, 31, 20 | grpsubeq0 19044 | . . 3
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇)) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) | 
| 33 | 25, 28, 30, 32 | syl3anc 1373 | . 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (((𝐹‘𝑈)(-g‘𝑇)(𝐹‘𝑉)) = (0g‘𝑇) ↔ (𝐹‘𝑈) = (𝐹‘𝑉))) | 
| 34 | 14, 23, 33 | 3bitrrd 306 | 1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ (𝑈 − 𝑉) ∈ 𝐾)) |