Step | Hyp | Ref
| Expression |
1 | | eldprdi.w |
. . . . . . . 8
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
2 | | eldprdi.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
3 | | eldprdi.2 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑆 = 𝐼) |
4 | | eldprdi.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
5 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 18234 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | 6 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
8 | | dprdfadd.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
9 | 1, 2, 3, 8, 5 | dprdff 18234 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝐼⟶(Base‘𝐺)) |
10 | 9 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) ∈ (Base‘𝐺)) |
11 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
13 | | dprdfsub.b |
. . . . . . 7
⊢ − =
(-g‘𝐺) |
14 | 5, 11, 12, 13 | grpsubval 17288 |
. . . . . 6
⊢ (((𝐹‘𝑘) ∈ (Base‘𝐺) ∧ (𝐻‘𝑘) ∈ (Base‘𝐺)) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
15 | 7, 10, 14 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
16 | 15 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
17 | 2, 3 | dprddomcld 18223 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
18 | 6 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) |
19 | 9 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝑘 ∈ 𝐼 ↦ (𝐻‘𝑘))) |
20 | 17, 7, 10, 18, 19 | offval2 6812 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐻) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘)))) |
21 | | fvex 6113 |
. . . . . 6
⊢
((invg‘𝐺)‘(𝐻‘𝑘)) ∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((invg‘𝐺)‘(𝐻‘𝑘)) ∈ V) |
23 | | dprdgrp 18227 |
. . . . . . . . . 10
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
24 | 2, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
25 | 5, 12, 24 | grpinvf1o 17308 |
. . . . . . . 8
⊢ (𝜑 →
(invg‘𝐺):(Base‘𝐺)–1-1-onto→(Base‘𝐺)) |
26 | | f1of 6050 |
. . . . . . . 8
⊢
((invg‘𝐺):(Base‘𝐺)–1-1-onto→(Base‘𝐺) → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
28 | 27 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝐺) =
(𝑥 ∈ (Base‘𝐺) ↦
((invg‘𝐺)‘𝑥))) |
29 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (𝐻‘𝑘) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐺)‘(𝐻‘𝑘))) |
30 | 10, 19, 28, 29 | fmptco 6303 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) = (𝑘 ∈ 𝐼 ↦ ((invg‘𝐺)‘(𝐻‘𝑘)))) |
31 | 17, 7, 22, 18, 30 | offval2 6812 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
32 | 16, 20, 31 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐻) = (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) |
33 | | eldprdi.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
34 | 33, 1, 2, 3, 8, 12 | dprdfinv 18241 |
. . . . . 6
⊢ (𝜑 →
(((invg‘𝐺)
∘ 𝐻) ∈ 𝑊 ∧ (𝐺 Σg
((invg‘𝐺)
∘ 𝐻)) =
((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
35 | 34 | simpld 474 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) ∈ 𝑊) |
36 | 33, 1, 2, 3, 4, 35,
11 | dprdfadd 18242 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻))))) |
37 | 36 | simpld 474 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) ∈ 𝑊) |
38 | 32, 37 | eqeltrd 2688 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐻) ∈ 𝑊) |
39 | 32 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
−
𝐻)) = (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)))) |
40 | 34 | simprd 478 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg
((invg‘𝐺)
∘ 𝐻)) =
((invg‘𝐺)‘(𝐺 Σg 𝐻))) |
41 | 40 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻))) = ((𝐺 Σg
𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
42 | 36 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻)))) |
43 | 5 | dprdssv 18238 |
. . . . . 6
⊢ (𝐺 DProd 𝑆) ⊆ (Base‘𝐺) |
44 | 33, 1, 2, 3, 4 | eldprdi 18240 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆)) |
45 | 43, 44 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (Base‘𝐺)) |
46 | 33, 1, 2, 3, 8 | eldprdi 18240 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (𝐺 DProd 𝑆)) |
47 | 43, 46 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) |
48 | 5, 11, 12, 13 | grpsubval 17288 |
. . . . 5
⊢ (((𝐺 Σg
𝐹) ∈ (Base‘𝐺) ∧ (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
49 | 45, 47, 48 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
50 | 41, 42, 49 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) |
51 | 39, 50 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
−
𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) |
52 | 38, 51 | jca 553 |
1
⊢ (𝜑 → ((𝐹 ∘𝑓 − 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘𝑓
−
𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))) |