Step | Hyp | Ref
| Expression |
1 | | gsumsub.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsumsub.z |
. . . 4
⊢ 0 =
(0g‘𝐺) |
3 | | eqid 2622 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | gsumsub.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Abel) |
5 | | ablcmn 18199 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
7 | | gsumsub.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | gsumsub.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
9 | | eqid 2622 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
10 | | ablgrp 18198 |
. . . . . . . 8
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
11 | 4, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
12 | 1, 9, 11 | grpinvf1o 17485 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝐺):𝐵–1-1-onto→𝐵) |
13 | | f1of 6137 |
. . . . . 6
⊢
((invg‘𝐺):𝐵–1-1-onto→𝐵 →
(invg‘𝐺):𝐵⟶𝐵) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 →
(invg‘𝐺):𝐵⟶𝐵) |
15 | | gsumsub.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
16 | | fco 6058 |
. . . . 5
⊢
(((invg‘𝐺):𝐵⟶𝐵 ∧ 𝐻:𝐴⟶𝐵) → ((invg‘𝐺) ∘ 𝐻):𝐴⟶𝐵) |
17 | 14, 15, 16 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻):𝐴⟶𝐵) |
18 | | gsumsub.fn |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 0 ) |
19 | | fvex 6201 |
. . . . . . 7
⊢
(0g‘𝐺) ∈ V |
20 | 2, 19 | eqeltri 2697 |
. . . . . 6
⊢ 0 ∈
V |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈ V) |
22 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
23 | 1, 22 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
25 | | gsumsub.hn |
. . . . 5
⊢ (𝜑 → 𝐻 finSupp 0 ) |
26 | 2, 9 | grpinvid 17476 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 0 ) = 0 ) |
27 | 11, 26 | syl 17 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)‘ 0 ) = 0 ) |
28 | 21, 15, 14, 7, 24, 25, 27 | fsuppco2 8308 |
. . . 4
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) finSupp 0
) |
29 | 1, 2, 3, 6, 7, 8, 17, 18, 28 | gsumadd 18323 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻)))) |
30 | 1, 2, 9, 4, 7, 15,
25 | gsuminv 18346 |
. . . 4
⊢ (𝜑 → (𝐺 Σg
((invg‘𝐺)
∘ 𝐻)) =
((invg‘𝐺)‘(𝐺 Σg 𝐻))) |
31 | 30 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻))) = ((𝐺 Σg
𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
32 | 29, 31 | eqtrd 2656 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
33 | 8 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
34 | 15 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐻‘𝑘) ∈ 𝐵) |
35 | | gsumsub.m |
. . . . . . 7
⊢ − =
(-g‘𝐺) |
36 | 1, 3, 9, 35 | grpsubval 17465 |
. . . . . 6
⊢ (((𝐹‘𝑘) ∈ 𝐵 ∧ (𝐻‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
37 | 33, 34, 36 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
38 | 37 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘))) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
39 | 8 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
40 | 15 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝑘 ∈ 𝐴 ↦ (𝐻‘𝑘))) |
41 | 7, 33, 34, 39, 40 | offval2 6914 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐻) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘)))) |
42 | | fvexd 6203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((invg‘𝐺)‘(𝐻‘𝑘)) ∈ V) |
43 | 14 | feqmptd 6249 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝐺) =
(𝑥 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑥))) |
44 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = (𝐻‘𝑘) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐺)‘(𝐻‘𝑘))) |
45 | 34, 40, 43, 44 | fmptco 6396 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) = (𝑘 ∈ 𝐴 ↦ ((invg‘𝐺)‘(𝐻‘𝑘)))) |
46 | 7, 33, 42, 39, 45 | offval2 6914 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
47 | 38, 41, 46 | 3eqtr4d 2666 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐻) = (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) |
48 | 47 | oveq2d 6666 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
−
𝐻)) = (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)))) |
49 | 1, 2, 6, 7, 8, 18 | gsumcl 18316 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) |
50 | 1, 2, 6, 7, 15, 25 | gsumcl 18316 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ 𝐵) |
51 | 1, 3, 9, 35 | grpsubval 17465 |
. . 3
⊢ (((𝐺 Σg
𝐹) ∈ 𝐵 ∧ (𝐺 Σg 𝐻) ∈ 𝐵) → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
52 | 49, 50, 51 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
53 | 32, 48, 52 | 3eqtr4d 2666 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
−
𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) |