Step | Hyp | Ref
| Expression |
1 | | dvnprod.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | dvnprod.x |
. . 3
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
3 | | dvnprod.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ Fin) |
4 | | dvnprod.h |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ) |
5 | | dvnprod.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | | dvnprod.dvnh |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻‘𝑡))‘𝑘):𝑋⟶ℂ) |
7 | | dvnprod.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥)) |
8 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑡 → (𝑑‘𝑢) = (𝑑‘𝑡)) |
9 | 8 | cbvsumv 14426 |
. . . . . . . . . . 11
⊢
Σ𝑢 ∈
𝑟 (𝑑‘𝑢) = Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) |
10 | 9 | eqeq1i 2627 |
. . . . . . . . . 10
⊢
(Σ𝑢 ∈
𝑟 (𝑑‘𝑢) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) → (Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚)) |
12 | 11 | rabbiia 3185 |
. . . . . . . 8
⊢ {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚} = {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚} |
13 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑒 → (𝑑‘𝑡) = (𝑒‘𝑡)) |
14 | 13 | sumeq2ad 14434 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑒 → Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = Σ𝑡 ∈ 𝑟 (𝑒‘𝑡)) |
15 | 14 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑑 = 𝑒 → (Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚)) |
16 | 15 | cbvrabv 3199 |
. . . . . . . 8
⊢ {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} |
17 | 12, 16 | eqtri 2644 |
. . . . . . 7
⊢ {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} |
18 | 17 | mpteq2i 4741 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚)
↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚}) = (𝑚 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚}) |
19 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛)) |
20 | 19 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
21 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) |
22 | 21 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((0...𝑚) ↑𝑚 𝑟) = ((0...𝑛) ↑𝑚 𝑟)) |
23 | | rabeq 3192 |
. . . . . . . . 9
⊢
(((0...𝑚)
↑𝑚 𝑟) = ((0...𝑛) ↑𝑚 𝑟) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
25 | 20, 24 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
26 | 25 | cbvmptv 4750 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑒 ∈
((0...𝑚)
↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
27 | 18, 26 | eqtri 2644 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚)
↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) |
28 | 27 | mpteq2i 4741 |
. . . 4
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚})) = (𝑟 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛})) |
29 | | sumeq1 14419 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑠 (𝑒‘𝑡)) |
30 | 29 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛)) |
31 | 30 | rabbidv 3189 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) |
32 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → ((0...𝑛) ↑𝑚 𝑟) = ((0...𝑛) ↑𝑚 𝑠)) |
33 | | rabeq 3192 |
. . . . . . . 8
⊢
(((0...𝑛)
↑𝑚 𝑟) = ((0...𝑛) ↑𝑚 𝑠) → {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) |
35 | 31, 34 | eqtrd 2656 |
. . . . . 6
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) |
36 | 35 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑟 = 𝑠 → (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) |
37 | 36 | cbvmptv 4750 |
. . . 4
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛})) = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) |
38 | 28, 37 | eqtri 2644 |
. . 3
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑𝑚 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚})) = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) |
39 | | dvnprod.c |
. . . 4
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) |
40 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡)) |
41 | 40 | sumeq2ad 14434 |
. . . . . . 7
⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑇 (𝑒‘𝑡)) |
42 | 41 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛)) |
43 | 42 | cbvrabv 3199 |
. . . . 5
⊢ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛} |
44 | 43 | mpteq2i 4741 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ {𝑐 ∈
((0...𝑛)
↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛}) |
45 | 39, 44 | eqtri 2644 |
. . 3
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛}) |
46 | 1, 2, 3, 4, 5, 6, 7, 38, 45 | dvnprodlem3 40163 |
. 2
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)))) |
47 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑐 → (𝑒‘𝑡) = (𝑐‘𝑡)) |
48 | 47 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑒 = 𝑐 → (!‘(𝑒‘𝑡)) = (!‘(𝑐‘𝑡))) |
49 | 48 | prodeq2ad 39824 |
. . . . . . . 8
⊢ (𝑒 = 𝑐 → ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡)) = ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) |
50 | 49 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑒 = 𝑐 → ((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) = ((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡)))) |
51 | 47 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑒 = 𝑐 → ((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡)) = ((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))) |
52 | 51 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑒 = 𝑐 → (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) |
53 | 52 | prodeq2ad 39824 |
. . . . . . 7
⊢ (𝑒 = 𝑐 → ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥) = ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) |
54 | 50, 53 | oveq12d 6668 |
. . . . . 6
⊢ (𝑒 = 𝑐 → (((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) |
55 | 54 | cbvsumv 14426 |
. . . . 5
⊢
Σ𝑒 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) |
56 | | eqid 2622 |
. . . . 5
⊢
Σ𝑐 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) |
57 | 55, 56 | eqtri 2644 |
. . . 4
⊢
Σ𝑒 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) |
58 | 57 | mpteq2i 4741 |
. . 3
⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) |
59 | 58 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) |
60 | 46, 59 | eqtrd 2656 |
1
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) |