Proof of Theorem ghminv
| Step | Hyp | Ref
| Expression |
| 1 | | ghmgrp1 19236 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
| 2 | | ghminv.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
| 3 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
| 5 | | ghminv.y |
. . . . . . 7
⊢ 𝑀 = (invg‘𝑆) |
| 6 | 2, 3, 4, 5 | grprinv 19008 |
. . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝑆)(𝑀‘𝑋)) = (0g‘𝑆)) |
| 7 | 1, 6 | sylan 580 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝑆)(𝑀‘𝑋)) = (0g‘𝑆)) |
| 8 | 7 | fveq2d 6910 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑋(+g‘𝑆)(𝑀‘𝑋))) = (𝐹‘(0g‘𝑆))) |
| 9 | 2, 5 | grpinvcl 19005 |
. . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝐵) |
| 10 | 1, 9 | sylan 580 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝐵) |
| 11 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑇) = (+g‘𝑇) |
| 12 | 2, 3, 11 | ghmlin 19239 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ (𝑀‘𝑋) ∈ 𝐵) → (𝐹‘(𝑋(+g‘𝑆)(𝑀‘𝑋))) = ((𝐹‘𝑋)(+g‘𝑇)(𝐹‘(𝑀‘𝑋)))) |
| 13 | 10, 12 | mpd3an3 1464 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑋(+g‘𝑆)(𝑀‘𝑋))) = ((𝐹‘𝑋)(+g‘𝑇)(𝐹‘(𝑀‘𝑋)))) |
| 14 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
| 15 | 4, 14 | ghmid 19240 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
| 17 | 8, 13, 16 | 3eqtr3d 2785 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → ((𝐹‘𝑋)(+g‘𝑇)(𝐹‘(𝑀‘𝑋))) = (0g‘𝑇)) |
| 18 | | ghmgrp2 19237 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) |
| 19 | 18 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → 𝑇 ∈ Grp) |
| 20 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
| 21 | 2, 20 | ghmf 19238 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) |
| 22 | 21 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ (Base‘𝑇)) |
| 23 | 21 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵⟶(Base‘𝑇)) |
| 24 | 23, 10 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) ∈ (Base‘𝑇)) |
| 25 | | ghminv.z |
. . . . 5
⊢ 𝑁 = (invg‘𝑇) |
| 26 | 20, 11, 14, 25 | grpinvid1 19009 |
. . . 4
⊢ ((𝑇 ∈ Grp ∧ (𝐹‘𝑋) ∈ (Base‘𝑇) ∧ (𝐹‘(𝑀‘𝑋)) ∈ (Base‘𝑇)) → ((𝑁‘(𝐹‘𝑋)) = (𝐹‘(𝑀‘𝑋)) ↔ ((𝐹‘𝑋)(+g‘𝑇)(𝐹‘(𝑀‘𝑋))) = (0g‘𝑇))) |
| 27 | 19, 22, 24, 26 | syl3anc 1373 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → ((𝑁‘(𝐹‘𝑋)) = (𝐹‘(𝑀‘𝑋)) ↔ ((𝐹‘𝑋)(+g‘𝑇)(𝐹‘(𝑀‘𝑋))) = (0g‘𝑇))) |
| 28 | 17, 27 | mpbird 257 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝐹‘𝑋)) = (𝐹‘(𝑀‘𝑋))) |
| 29 | 28 | eqcomd 2743 |
1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋))) |