Proof of Theorem ghmsub
Step | Hyp | Ref
| Expression |
1 | | ghmgrp1 18624 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
2 | 1 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑆 ∈ Grp) |
3 | | simp3 1140 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → 𝑉 ∈ 𝐵) |
4 | | ghmsub.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
5 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝑆) = (invg‘𝑆) |
6 | 4, 5 | grpinvcl 18415 |
. . . . 5
⊢ ((𝑆 ∈ Grp ∧ 𝑉 ∈ 𝐵) → ((invg‘𝑆)‘𝑉) ∈ 𝐵) |
7 | 2, 3, 6 | syl2anc 587 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((invg‘𝑆)‘𝑉) ∈ 𝐵) |
8 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) |
9 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑇) = (+g‘𝑇) |
10 | 4, 8, 9 | ghmlin 18627 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ ((invg‘𝑆)‘𝑉) ∈ 𝐵) → (𝐹‘(𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉))) = ((𝐹‘𝑈)(+g‘𝑇)(𝐹‘((invg‘𝑆)‘𝑉)))) |
11 | 7, 10 | syld3an3 1411 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉))) = ((𝐹‘𝑈)(+g‘𝑇)(𝐹‘((invg‘𝑆)‘𝑉)))) |
12 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝑇) = (invg‘𝑇) |
13 | 4, 5, 12 | ghminv 18629 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ 𝐵) → (𝐹‘((invg‘𝑆)‘𝑉)) = ((invg‘𝑇)‘(𝐹‘𝑉))) |
14 | 13 | 3adant2 1133 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘((invg‘𝑆)‘𝑉)) = ((invg‘𝑇)‘(𝐹‘𝑉))) |
15 | 14 | oveq2d 7229 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈)(+g‘𝑇)(𝐹‘((invg‘𝑆)‘𝑉))) = ((𝐹‘𝑈)(+g‘𝑇)((invg‘𝑇)‘(𝐹‘𝑉)))) |
16 | 11, 15 | eqtrd 2777 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉))) = ((𝐹‘𝑈)(+g‘𝑇)((invg‘𝑇)‘(𝐹‘𝑉)))) |
17 | | ghmsub.m |
. . . . 5
⊢ − =
(-g‘𝑆) |
18 | 4, 8, 5, 17 | grpsubval 18413 |
. . . 4
⊢ ((𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝑈 − 𝑉) = (𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉))) |
19 | 18 | fveq2d 6721 |
. . 3
⊢ ((𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = (𝐹‘(𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉)))) |
20 | 19 | 3adant1 1132 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = (𝐹‘(𝑈(+g‘𝑆)((invg‘𝑆)‘𝑉)))) |
21 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
22 | 4, 21 | ghmf 18626 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) |
23 | | ffvelrn 6902 |
. . . . . 6
⊢ ((𝐹:𝐵⟶(Base‘𝑇) ∧ 𝑈 ∈ 𝐵) → (𝐹‘𝑈) ∈ (Base‘𝑇)) |
24 | | ffvelrn 6902 |
. . . . . 6
⊢ ((𝐹:𝐵⟶(Base‘𝑇) ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑉) ∈ (Base‘𝑇)) |
25 | 23, 24 | anim12dan 622 |
. . . . 5
⊢ ((𝐹:𝐵⟶(Base‘𝑇) ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇))) |
26 | 22, 25 | sylan 583 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇))) |
27 | 26 | 3impb 1117 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇))) |
28 | | ghmsub.n |
. . . 4
⊢ 𝑁 = (-g‘𝑇) |
29 | 21, 9, 12, 28 | grpsubval 18413 |
. . 3
⊢ (((𝐹‘𝑈) ∈ (Base‘𝑇) ∧ (𝐹‘𝑉) ∈ (Base‘𝑇)) → ((𝐹‘𝑈)𝑁(𝐹‘𝑉)) = ((𝐹‘𝑈)(+g‘𝑇)((invg‘𝑇)‘(𝐹‘𝑉)))) |
30 | 27, 29 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈)𝑁(𝐹‘𝑉)) = ((𝐹‘𝑈)(+g‘𝑇)((invg‘𝑇)‘(𝐹‘𝑉)))) |
31 | 16, 20, 30 | 3eqtr4d 2787 |
1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉))) |