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 2739 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 19266 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | 6 | ffvelrnda 6874 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (Base‘𝐺)) |
8 | | dprdfadd.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
9 | 1, 2, 3, 8, 5 | dprdff 19266 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝐼⟶(Base‘𝐺)) |
10 | 9 | ffvelrnda 6874 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) ∈ (Base‘𝐺)) |
11 | | eqid 2739 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | | eqid 2739 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
13 | | dprdfsub.b |
. . . . . . 7
⊢ − =
(-g‘𝐺) |
14 | 5, 11, 12, 13 | grpsubval 18280 |
. . . . . 6
⊢ (((𝐹‘𝑘) ∈ (Base‘𝐺) ∧ (𝐻‘𝑘) ∈ (Base‘𝐺)) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
15 | 7, 10, 14 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐻‘𝑘)) = ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘)))) |
16 | 15 | mpteq2dva 5135 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
17 | 2, 3 | dprddomcld 19255 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
18 | 6 | feqmptd 6750 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) |
19 | 9 | feqmptd 6750 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝑘 ∈ 𝐼 ↦ (𝐻‘𝑘))) |
20 | 17, 7, 10, 18, 19 | offval2 7457 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f − 𝐻) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘) − (𝐻‘𝑘)))) |
21 | | fvexd 6702 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((invg‘𝐺)‘(𝐻‘𝑘)) ∈ V) |
22 | | dprdgrp 19259 |
. . . . . . . . . 10
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
23 | 2, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
24 | 5, 12, 23 | grpinvf1o 18300 |
. . . . . . . 8
⊢ (𝜑 →
(invg‘𝐺):(Base‘𝐺)–1-1-onto→(Base‘𝐺)) |
25 | | f1of 6631 |
. . . . . . . 8
⊢
((invg‘𝐺):(Base‘𝐺)–1-1-onto→(Base‘𝐺) → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
27 | 26 | feqmptd 6750 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝐺) =
(𝑥 ∈ (Base‘𝐺) ↦
((invg‘𝐺)‘𝑥))) |
28 | | fveq2 6687 |
. . . . . 6
⊢ (𝑥 = (𝐻‘𝑘) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐺)‘(𝐻‘𝑘))) |
29 | 10, 19, 27, 28 | fmptco 6914 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) = (𝑘 ∈ 𝐼 ↦ ((invg‘𝐺)‘(𝐻‘𝑘)))) |
30 | 17, 7, 21, 18, 29 | offval2 7457 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)(+g‘𝐺)((invg‘𝐺)‘(𝐻‘𝑘))))) |
31 | 16, 20, 30 | 3eqtr4d 2784 |
. . 3
⊢ (𝜑 → (𝐹 ∘f − 𝐻) = (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) |
32 | | eldprdi.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
33 | 32, 1, 2, 3, 8, 12 | dprdfinv 19273 |
. . . . . 6
⊢ (𝜑 →
(((invg‘𝐺)
∘ 𝐻) ∈ 𝑊 ∧ (𝐺 Σg
((invg‘𝐺)
∘ 𝐻)) =
((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
34 | 33 | simpld 498 |
. . . . 5
⊢ (𝜑 →
((invg‘𝐺)
∘ 𝐻) ∈ 𝑊) |
35 | 32, 1, 2, 3, 4, 34,
11 | dprdfadd 19274 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻))))) |
36 | 35 | simpld 498 |
. . 3
⊢ (𝜑 → (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)) ∈ 𝑊) |
37 | 31, 36 | eqeltrd 2834 |
. 2
⊢ (𝜑 → (𝐹 ∘f − 𝐻) ∈ 𝑊) |
38 | 31 | oveq2d 7199 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f − 𝐻)) = (𝐺 Σg (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻)))) |
39 | 33 | simprd 499 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg
((invg‘𝐺)
∘ 𝐻)) =
((invg‘𝐺)‘(𝐺 Σg 𝐻))) |
40 | 39 | oveq2d 7199 |
. . . 4
⊢ (𝜑 → ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻))) = ((𝐺 Σg
𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
41 | 35 | simprd 499 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹)(+g‘𝐺)(𝐺 Σg
((invg‘𝐺)
∘ 𝐻)))) |
42 | 5 | dprdssv 19270 |
. . . . . 6
⊢ (𝐺 DProd 𝑆) ⊆ (Base‘𝐺) |
43 | 32, 1, 2, 3, 4 | eldprdi 19272 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆)) |
44 | 42, 43 | sseldi 3885 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (Base‘𝐺)) |
45 | 32, 1, 2, 3, 8 | eldprdi 19272 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (𝐺 DProd 𝑆)) |
46 | 42, 45 | sseldi 3885 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) |
47 | 5, 11, 12, 13 | grpsubval 18280 |
. . . . 5
⊢ (((𝐺 Σg
𝐹) ∈ (Base‘𝐺) ∧ (𝐺 Σg 𝐻) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
48 | 44, 46, 47 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)) = ((𝐺 Σg 𝐹)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝐻)))) |
49 | 40, 41, 48 | 3eqtr4d 2784 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f
(+g‘𝐺)((invg‘𝐺) ∘ 𝐻))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) |
50 | 38, 49 | eqtrd 2774 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) |
51 | 37, 50 | jca 515 |
1
⊢ (𝜑 → ((𝐹 ∘f − 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))) |