| 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 6905 | . . . . . . . . . . 11
⊢ (𝑢 = 𝑡 → (𝑑‘𝑢) = (𝑑‘𝑡)) | 
| 9 | 8 | cbvsumv 15733 | . . . . . . . . . 10
⊢
Σ𝑢 ∈
𝑟 (𝑑‘𝑢) = Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) | 
| 10 | 9 | eqeq1i 2741 | . . . . . . . . 9
⊢
(Σ𝑢 ∈
𝑟 (𝑑‘𝑢) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚) | 
| 11 | 10 | rabbii 3441 | . . . . . . . 8
⊢ {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚} = {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚} | 
| 12 |  | fveq1 6904 | . . . . . . . . . . 11
⊢ (𝑑 = 𝑒 → (𝑑‘𝑡) = (𝑒‘𝑡)) | 
| 13 | 12 | sumeq2sdv 15740 | . . . . . . . . . 10
⊢ (𝑑 = 𝑒 → Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = Σ𝑡 ∈ 𝑟 (𝑒‘𝑡)) | 
| 14 | 13 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑑 = 𝑒 → (Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚)) | 
| 15 | 14 | cbvrabv 3446 | . . . . . . . 8
⊢ {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑑‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} | 
| 16 | 11, 15 | eqtri 2764 | . . . . . . 7
⊢ {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} | 
| 17 | 16 | mpteq2i 5246 | . . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚}) = (𝑚 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚}) | 
| 18 |  | eqeq2 2748 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛)) | 
| 19 | 18 | rabbidv 3443 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 20 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) | 
| 21 | 20 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((0...𝑚) ↑m 𝑟) = ((0...𝑛) ↑m 𝑟)) | 
| 22 |  | rabeq 3450 | . . . . . . . . 9
⊢
(((0...𝑚)
↑m 𝑟) =
((0...𝑛) ↑m
𝑟) → {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 23 | 21, 22 | syl 17 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 24 | 19, 23 | eqtrd 2776 | . . . . . . 7
⊢ (𝑚 = 𝑛 → {𝑒 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 25 | 24 | cbvmptv 5254 | . . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑒 ∈
((0...𝑚) ↑m
𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 26 | 17, 25 | eqtri 2764 | . . . . 5
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) | 
| 27 | 26 | mpteq2i 5246 | . . . 4
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚})) = (𝑟 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛})) | 
| 28 |  | sumeq1 15726 | . . . . . . . . 9
⊢ (𝑟 = 𝑠 → Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑠 (𝑒‘𝑡)) | 
| 29 | 28 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑟 = 𝑠 → (Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛)) | 
| 30 | 29 | rabbidv 3443 | . . . . . . 7
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) | 
| 31 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑟 = 𝑠 → ((0...𝑛) ↑m 𝑟) = ((0...𝑛) ↑m 𝑠)) | 
| 32 |  | rabeq 3450 | . . . . . . . 8
⊢
(((0...𝑛)
↑m 𝑟) =
((0...𝑛) ↑m
𝑠) → {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) | 
| 33 | 31, 32 | syl 17 | . . . . . . 7
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) | 
| 34 | 30, 33 | eqtrd 2776 | . . . . . 6
⊢ (𝑟 = 𝑠 → {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛}) | 
| 35 | 34 | mpteq2dv 5243 | . . . . 5
⊢ (𝑟 = 𝑠 → (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) | 
| 36 | 35 | cbvmptv 5254 | . . . 4
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑟) ∣ Σ𝑡 ∈ 𝑟 (𝑒‘𝑡) = 𝑛})) = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) | 
| 37 | 27, 36 | eqtri 2764 | . . 3
⊢ (𝑟 ∈ 𝒫 𝑇 ↦ (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m 𝑟) ∣ Σ𝑢 ∈ 𝑟 (𝑑‘𝑢) = 𝑚})) = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑒‘𝑡) = 𝑛})) | 
| 38 |  | dvnprod.c | . . . 4
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) | 
| 39 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡)) | 
| 40 | 39 | sumeq2sdv 15740 | . . . . . . 7
⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑇 (𝑒‘𝑡)) | 
| 41 | 40 | eqeq1d 2738 | . . . . . 6
⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛)) | 
| 42 | 41 | cbvrabv 3446 | . . . . 5
⊢ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛} = {𝑒 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛} | 
| 43 | 42 | mpteq2i 5246 | . . . 4
⊢ (𝑛 ∈ ℕ0
↦ {𝑐 ∈
((0...𝑛) ↑m
𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛}) | 
| 44 | 38, 43 | eqtri 2764 | . . 3
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑒‘𝑡) = 𝑛}) | 
| 45 | 1, 2, 3, 4, 5, 6, 7, 37, 44 | dvnprodlem3 45968 | . 2
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)))) | 
| 46 |  | fveq1 6904 | . . . . . . . . . 10
⊢ (𝑒 = 𝑐 → (𝑒‘𝑡) = (𝑐‘𝑡)) | 
| 47 | 46 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑒 = 𝑐 → (!‘(𝑒‘𝑡)) = (!‘(𝑐‘𝑡))) | 
| 48 | 47 | prodeq2ad 45612 | . . . . . . . 8
⊢ (𝑒 = 𝑐 → ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡)) = ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) | 
| 49 | 48 | oveq2d 7448 | . . . . . . 7
⊢ (𝑒 = 𝑐 → ((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) = ((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡)))) | 
| 50 | 46 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑒 = 𝑐 → ((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡)) = ((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))) | 
| 51 | 50 | fveq1d 6907 | . . . . . . . 8
⊢ (𝑒 = 𝑐 → (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) | 
| 52 | 51 | prodeq2ad 45612 | . . . . . . 7
⊢ (𝑒 = 𝑐 → ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥) = ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) | 
| 53 | 49, 52 | oveq12d 7450 | . . . . . 6
⊢ (𝑒 = 𝑐 → (((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) | 
| 54 | 53 | cbvsumv 15733 | . . . . 5
⊢
Σ𝑒 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) | 
| 55 |  | eqid 2736 | . . . . 5
⊢
Σ𝑐 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) | 
| 56 | 54, 55 | eqtri 2764 | . . . 4
⊢
Σ𝑒 ∈
(𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) | 
| 57 | 56 | mpteq2i 5246 | . . 3
⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) | 
| 58 | 57 | a1i 11 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑒 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑒‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑒‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) | 
| 59 | 45, 58 | eqtrd 2776 | 1
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) |