Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem3 Structured version   Visualization version   GIF version

Theorem dvnprodlem3 40801
Description: The multinomial formula for the 𝑘-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem3.s (𝜑𝑆 ∈ {ℝ, ℂ})
dvnprodlem3.x (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
dvnprodlem3.t (𝜑𝑇 ∈ Fin)
dvnprodlem3.h ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
dvnprodlem3.n (𝜑𝑁 ∈ ℕ0)
dvnprodlem3.dvnh ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
dvnprodlem3.f 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
dvnprodlem3.d 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
dvnprodlem3.c 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
Assertion
Ref Expression
dvnprodlem3 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Distinct variable groups:   𝐶,𝑐   𝐷,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝐹,𝑠   𝐻,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝑁,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝑆,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝑇,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝑋,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥   𝜑,𝑐,𝑗,𝑡,𝑛,𝑠,𝑥
Allowed substitution hints:   𝐶(𝑥,𝑡,𝑗,𝑛,𝑠)   𝐹(𝑥,𝑡,𝑗,𝑛,𝑐)

Proof of Theorem dvnprodlem3
Dummy variables 𝑑 𝑘 𝑙 𝑟 𝑧 𝑦 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodeq1 14922 . . . . . . . . 9 (𝑠 = ∅ → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))
21mpteq2dv 4904 . . . . . . . 8 (𝑠 = ∅ → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))
32oveq2d 6858 . . . . . . 7 (𝑠 = ∅ → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))))
43fveq1d 6377 . . . . . 6 (𝑠 = ∅ → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘))
5 fveq2 6375 . . . . . . . . . 10 (𝑠 = ∅ → (𝐷𝑠) = (𝐷‘∅))
65fveq1d 6377 . . . . . . . . 9 (𝑠 = ∅ → ((𝐷𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
76sumeq1d 14716 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
8 prodeq1 14922 . . . . . . . . . . 11 (𝑠 = ∅ → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐𝑡)))
98oveq2d 6858 . . . . . . . . . 10 (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
10 prodeq1 14922 . . . . . . . . . 10 (𝑠 = ∅ → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
119, 10oveq12d 6860 . . . . . . . . 9 (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1211sumeq2ad 14719 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
137, 12eqtrd 2799 . . . . . . 7 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1413mpteq2dv 4904 . . . . . 6 (𝑠 = ∅ → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
154, 14eqeq12d 2780 . . . . 5 (𝑠 = ∅ → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
1615ralbidv 3133 . . . 4 (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
17 prodeq1 14922 . . . . . . . . 9 (𝑠 = 𝑟 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))
1817mpteq2dv 4904 . . . . . . . 8 (𝑠 = 𝑟 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
1918oveq2d 6858 . . . . . . 7 (𝑠 = 𝑟 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
2019fveq1d 6377 . . . . . 6 (𝑠 = 𝑟 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘))
21 fveq2 6375 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝐷𝑠) = (𝐷𝑟))
2221fveq1d 6377 . . . . . . . . 9 (𝑠 = 𝑟 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑟)‘𝑘))
2322sumeq1d 14716 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
24 prodeq1 14922 . . . . . . . . . . 11 (𝑠 = 𝑟 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑟 (!‘(𝑐𝑡)))
2524oveq2d 6858 . . . . . . . . . 10 (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
26 prodeq1 14922 . . . . . . . . . 10 (𝑠 = 𝑟 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
2725, 26oveq12d 6860 . . . . . . . . 9 (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2827sumeq2ad 14719 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2923, 28eqtrd 2799 . . . . . . 7 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
3029mpteq2dv 4904 . . . . . 6 (𝑠 = 𝑟 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
3120, 30eqeq12d 2780 . . . . 5 (𝑠 = 𝑟 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
3231ralbidv 3133 . . . 4 (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
33 prodeq1 14922 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))
3433mpteq2dv 4904 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))
3534oveq2d 6858 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))))
3635fveq1d 6377 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
37 fveq2 6375 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
3837fveq1d 6377 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
3938sumeq1d 14716 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
40 prodeq1 14922 . . . . . . . . . . 11 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡)))
4140oveq2d 6858 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
42 prodeq1 14922 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
4341, 42oveq12d 6860 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4443sumeq2ad 14719 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4539, 44eqtrd 2799 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4645mpteq2dv 4904 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
4736, 46eqeq12d 2780 . . . . 5 (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
4847ralbidv 3133 . . . 4 (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
49 prodeq1 14922 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5049mpteq2dv 4904 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
51 dvnprodlem3.f . . . . . . . . . . 11 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5251a1i 11 . . . . . . . . . 10 (𝑠 = 𝑇𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
5352eqcomd 2771 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)) = 𝐹)
5450, 53eqtrd 2799 . . . . . . . 8 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = 𝐹)
5554oveq2d 6858 . . . . . . 7 (𝑠 = 𝑇 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 𝐹))
5655fveq1d 6377 . . . . . 6 (𝑠 = 𝑇 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘))
57 fveq2 6375 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝐷𝑠) = (𝐷𝑇))
5857fveq1d 6377 . . . . . . . . 9 (𝑠 = 𝑇 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑇)‘𝑘))
5958sumeq1d 14716 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
60 prodeq1 14922 . . . . . . . . . . 11 (𝑠 = 𝑇 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑇 (!‘(𝑐𝑡)))
6160oveq2d 6858 . . . . . . . . . 10 (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
62 prodeq1 14922 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
6361, 62oveq12d 6860 . . . . . . . . 9 (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6463sumeq2ad 14719 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6559, 64eqtrd 2799 . . . . . . 7 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6665mpteq2dv 4904 . . . . . 6 (𝑠 = 𝑇 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
6756, 66eqeq12d 2780 . . . . 5 (𝑠 = 𝑇 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
6867ralbidv 3133 . . . 4 (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
69 prod0 14956 . . . . . . . . . . . . 13 𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥) = 1
7069mpteq2i 4900 . . . . . . . . . . . 12 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ 1)
7170oveq2i 6853 . . . . . . . . . . 11 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1))
7271a1i 11 . . . . . . . . . 10 (𝑘 = 0 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1)))
73 id 22 . . . . . . . . . 10 (𝑘 = 0 → 𝑘 = 0)
7472, 73fveq12d 6382 . . . . . . . . 9 (𝑘 = 0 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
7574adantl 473 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
76 dvnprodlem3.s . . . . . . . . . . 11 (𝜑𝑆 ∈ {ℝ, ℂ})
77 recnprss 23959 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
7876, 77syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
79 1cnd 10288 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 1 ∈ ℂ)
8079fmpttd 6575 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ 1):𝑋⟶ℂ)
81 1re 10293 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
8281rgenw 3071 . . . . . . . . . . . . . . . 16 𝑥𝑋 1 ∈ ℝ
83 dmmptg 5818 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 1 ∈ ℝ → dom (𝑥𝑋 ↦ 1) = 𝑋)
8482, 83ax-mp 5 . . . . . . . . . . . . . . 15 dom (𝑥𝑋 ↦ 1) = 𝑋
8584a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑥𝑋 ↦ 1) = 𝑋)
8685feq2d 6209 . . . . . . . . . . . . 13 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ↔ (𝑥𝑋 ↦ 1):𝑋⟶ℂ))
8780, 86mpbird 248 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ)
88 restsspw 16358 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆
89 dvnprodlem3.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
9088, 89sseldi 3759 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ 𝒫 𝑆)
91 elpwi 4325 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝒫 𝑆𝑋𝑆)
9290, 91syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝑆)
9385, 92eqsstrd 3799 . . . . . . . . . . . 12 (𝜑 → dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)
9487, 93jca 507 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆))
95 cnex 10270 . . . . . . . . . . . . 13 ℂ ∈ V
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
97 elpm2g 8077 . . . . . . . . . . . 12 ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9896, 76, 97syl2anc 579 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9994, 98mpbird 248 . . . . . . . . . 10 (𝜑 → (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆))
100 dvn0 23978 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
10178, 99, 100syl2anc 579 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
102101adantr 472 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
103 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
104103adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105 dvnprodlem3.d . . . . . . . . . . . . . . . . . 18 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
106105a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
107 oveq2 6850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 ∅))
108 elmapfn 8083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 Fn ∅)
109 fn0 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 Fn ∅ ↔ 𝑥 = ∅)
110108, 109sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 = ∅)
111 velsn 4350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
112110, 111sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 ∈ {∅})
113111biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ {∅} → 𝑥 = ∅)
114 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = ∅ → 𝑥 = ∅)
115 f0 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅:∅⟶(0...𝑛)
116 ovex 6874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0...𝑛) ∈ V
117 0ex 4950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ ∈ V
118116, 117elmap 8089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ ((0...𝑛) ↑𝑚 ∅) ↔ ∅:∅⟶(0...𝑛))
119115, 118mpbir 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅ ∈ ((0...𝑛) ↑𝑚 ∅)
120119a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑𝑚 ∅))
121114, 120eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
122113, 121syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
123112, 122impbii 200 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
124123ax-gen 1890 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
125 dfcleq 2759 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑𝑚 ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅}))
126124, 125mpbir 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝑛) ↑𝑚 ∅) = {∅}
127126a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 ∅) = {∅})
128107, 127eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = {∅})
129 rabeq 3341 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑛) ↑𝑚 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
130128, 129syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
131 sumeq1 14704 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ ∅ (𝑐𝑡))
132131eqeq1d 2767 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛))
133132rabbidv 3338 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
134130, 133eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
135134mpteq2dv 4904 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
136135adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 = ∅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
137 0elpw 4992 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑇
138137a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ ∈ 𝒫 𝑇)
139 nn0ex 11545 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
140139mptex 6679 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V
141140a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V)
142106, 136, 138, 141fvmptd 6477 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
143 eqeq2 2776 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0))
144143rabbidv 3338 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
145144adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
146 0nn0 11555 . . . . . . . . . . . . . . . . 17 0 ∈ ℕ0
147146a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℕ0)
148 p0ex 5019 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
149148rabex 4973 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V
150149a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V)
151142, 145, 147, 150fvmptd 6477 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
152151adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
153 snidg 4364 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ V → ∅ ∈ {∅})
154117, 153ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ {∅}
155 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 0 = 0
156154, 155pm3.2i 462 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {∅} ∧ 0 = 0)
157 sum0 14737 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑡 ∈ ∅ (𝑐𝑡) = 0
158157a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
159158eqeq1d 2767 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 0 ↔ 0 = 0))
160159elrab 3519 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
161156, 160mpbir 222 . . . . . . . . . . . . . . . . . 18 ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
162161n0ii 4087 . . . . . . . . . . . . . . . . 17 ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅
163 eqid 2765 . . . . . . . . . . . . . . . . . 18 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
164 rabrsn 4414 . . . . . . . . . . . . . . . . . 18 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}))
165163, 164ax-mp 5 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
166162, 165mtpor 1865 . . . . . . . . . . . . . . . 16 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}
167166a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
168 iftrue 4249 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
169168adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
170167, 169eqtr4d 2802 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
171104, 152, 1703eqtrd 2803 . . . . . . . . . . . . 13 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
172171, 169eqtrd 2799 . . . . . . . . . . . 12 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
173172sumeq1d 14716 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
174 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘𝑘) = (!‘0))
175 fac0 13267 . . . . . . . . . . . . . . . . . . 19 (!‘0) = 1
176175a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘0) = 1)
177174, 176eqtrd 2799 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (!‘𝑘) = 1)
178177oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
179 prod0 14956 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ ∅ (!‘(𝑐𝑡)) = 1
180179oveq2i 6853 . . . . . . . . . . . . . . . . 17 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / 1)
181 1div1e1 10971 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
182180, 181eqtri 2787 . . . . . . . . . . . . . . . 16 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1
183178, 182syl6eq 2815 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1)
184 prod0 14956 . . . . . . . . . . . . . . . 16 𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1
185184a1i 11 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1)
186183, 185oveq12d 6860 . . . . . . . . . . . . . 14 (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
187186ad2antlr 718 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
188 1t1e1 11440 . . . . . . . . . . . . . 14 (1 · 1) = 1
189188a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
190187, 189eqtrd 2799 . . . . . . . . . . . 12 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
191190sumeq2dv 14718 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
192 ax-1cn 10247 . . . . . . . . . . . . 13 1 ∈ ℂ
193 eqidd 2766 . . . . . . . . . . . . . 14 (𝑐 = ∅ → 1 = 1)
194193sumsn 14760 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
195117, 192, 194mp2an 683 . . . . . . . . . . . 12 Σ𝑐 ∈ {∅}1 = 1
196195a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
197173, 191, 1963eqtrd 2803 . . . . . . . . . 10 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
198197mpteq2dv 4904 . . . . . . . . 9 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ 1))
199198eqcomd 2771 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
20075, 102, 1993eqtrd 2803 . . . . . . 7 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
201200a1d 25 . . . . . 6 ((𝜑𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
20271fveq1i 6376 . . . . . . . . 9 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘)
203202a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘))
20476adantr 472 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
205204adantr 472 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
20689adantr 472 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
207206adantr 472 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
208192a1i 11 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
209 elfznn0 12640 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
210209adantl 473 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
211 neqne 2945 . . . . . . . . . . . . 13 𝑘 = 0 → 𝑘 ≠ 0)
212211adantr 472 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
213210, 212jca 507 . . . . . . . . . . 11 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ0𝑘 ≠ 0))
214 elnnne0 11554 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
215213, 214sylibr 225 . . . . . . . . . 10 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
216215adantll 705 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
217205, 207, 208, 216dvnmptconst 40794 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘) = (𝑥𝑋 ↦ 0))
218142ad2antrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
219 eqeq2 2776 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘))
220219rabbidv 3338 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
221220adantl 473 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
222 eqidd 2766 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 𝑘)
223 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
224223eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = Σ𝑡 ∈ ∅ (𝑐𝑡))
225157a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
226222, 224, 2253eqtrd 2803 . . . . . . . . . . . . . . . . . . . . 21 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 0)
227226adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
228227adantll 705 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
229 simpll 783 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → ¬ 𝑘 = 0)
230228, 229pm2.65da 851 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
231230ralrimiva 3113 . . . . . . . . . . . . . . . . 17 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
232 rabeq0 4121 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
233231, 232sylibr 225 . . . . . . . . . . . . . . . 16 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
234233adantr 472 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
235221, 234eqtrd 2799 . . . . . . . . . . . . . 14 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
236235adantll 705 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
237236adantlr 706 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
238209adantl 473 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
239117a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
240218, 237, 238, 239fvmptd 6477 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
241240sumeq1d 14716 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
242 sum0 14737 . . . . . . . . . . 11 Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0
243242a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0)
244241, 243eqtr2d 2800 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
245244mpteq2dv 4904 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
246203, 217, 2453eqtrd 2803 . . . . . . 7 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
247246ex 401 . . . . . 6 ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
248201, 247pm2.61dan 847 . . . . 5 (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
249248ralrimiv 3112 . . . 4 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
250 simpll 783 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))))
251 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑡)‘𝑦))
252251prodeq2ad 40462 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑦))
253 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (𝐻𝑡) = (𝐻𝑢))
254253fveq1d 6377 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑢)‘𝑦))
255254cbvprodv 14929 . . . . . . . . . . . . . . . . 17 𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)
256255a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
257252, 256eqtrd 2799 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
258257cbvmptv 4909 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)) = (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
259258oveq2i 6853 . . . . . . . . . . . . 13 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))
260259fveq1i 6376 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘)
261 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → (𝑐𝑡) = (𝑐𝑢))
262261fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑢)))
263262cbvprodv 14929 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (!‘(𝑐𝑡)) = ∏𝑢𝑟 (!‘(𝑐𝑢))
264263oveq2i 6853 . . . . . . . . . . . . . . . . 17 ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢)))
265264a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))))
266 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
267266prodeq2ad 40462 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
268253oveq2d 6858 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑢 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑢)))
269268, 261fveq12d 6382 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)))
270269fveq1d 6377 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
271270cbvprodv 14929 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)
272271a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
273267, 272eqtrd 2799 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
274265, 273oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
275274sumeq2ad 14719 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
276 fveq1 6374 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → (𝑐𝑢) = (𝑑𝑢))
277276fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (!‘(𝑐𝑢)) = (!‘(𝑑𝑢)))
278277prodeq2ad 40462 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → ∏𝑢𝑟 (!‘(𝑐𝑢)) = ∏𝑢𝑟 (!‘(𝑑𝑢)))
279278oveq2d 6858 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))))
280276fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢)))
281280fveq1d 6377 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
282281prodeq2ad 40462 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
283279, 282oveq12d 6860 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
284283cbvsumv 14711 . . . . . . . . . . . . . . 15 Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
285284a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
286275, 285eqtrd 2799 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
287286cbvmptv 4909 . . . . . . . . . . . 12 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
288260, 287eqeq12i 2779 . . . . . . . . . . 11 (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
289288ralbii 3127 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
290289biimpi 207 . . . . . . . . 9 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
291290ad2antlr 718 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
292 simpr 477 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
29376ad3antrrr 721 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
29489ad3antrrr 721 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
295 dvnprodlem3.t . . . . . . . . . 10 (𝜑𝑇 ∈ Fin)
296295ad3antrrr 721 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
297 simp-4l 801 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝜑)
298 simpr 477 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝑡𝑇)
299 dvnprodlem3.h . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
300297, 298, 299syl2anc 579 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
301 dvnprodlem3.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
302301ad3antrrr 721 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
303 simplll 791 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
3043033ad2ant1 1163 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝜑)
305 simp2 1167 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝑡𝑇)
306 simp3 1168 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ∈ (0...𝑁))
307 eleq1w 2827 . . . . . . . . . . . . 13 (𝑗 = → (𝑗 ∈ (0...𝑁) ↔ ∈ (0...𝑁)))
3083073anbi3d 1566 . . . . . . . . . . . 12 (𝑗 = → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∈ (0...𝑁))))
309 fveq2 6375 . . . . . . . . . . . . 13 (𝑗 = → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘))
310309feq1d 6208 . . . . . . . . . . . 12 (𝑗 = → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ))
311308, 310imbi12d 335 . . . . . . . . . . 11 (𝑗 = → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)))
312 dvnprodlem3.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
313311, 312chvarv 2369 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
314304, 305, 306, 313syl3anc 1490 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
315 simprl 787 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑟𝑇)
316315ad2antrr 717 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟𝑇)
317 simprr 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑧 ∈ (𝑇𝑟))
318317ad2antrr 717 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇𝑟))
319259eqcomi 2774 . . . . . . . . . . . . . . 15 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
320319a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
321 id 22 . . . . . . . . . . . . . 14 (𝑘 = 𝑙𝑘 = 𝑙)
322320, 321fveq12d 6382 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙))
323287eqcomi 2774 . . . . . . . . . . . . . . 15 (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
324323a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
325 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
326325oveq1d 6857 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
327326oveq1d 6857 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
328327sumeq2ad 14719 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
329 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝐷𝑟)‘𝑘) = ((𝐷𝑟)‘𝑙))
330329sumeq1d 14716 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
331328, 330eqtrd 2799 . . . . . . . . . . . . . . 15 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
332331mpteq2dv 4904 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
333324, 332eqtrd 2799 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
334322, 333eqeq12d 2780 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
335334cbvralv 3319 . . . . . . . . . . 11 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
336335biimpi 207 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
337336ad2antlr 718 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
338 simpr 477 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
339 fveq1 6374 . . . . . . . . . . . 12 (𝑑 = 𝑐 → (𝑑𝑧) = (𝑐𝑧))
340339oveq2d 6858 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑗 − (𝑑𝑧)) = (𝑗 − (𝑐𝑧)))
341 reseq1 5559 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑑𝑟) = (𝑐𝑟))
342340, 341opeq12d 4567 . . . . . . . . . 10 (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩ = ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
343342cbvmptv 4909 . . . . . . . . 9 (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
344293, 294, 296, 300, 302, 314, 105, 316, 318, 337, 338, 343dvnprodlem2 40800 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
345250, 291, 292, 344syl21anc 866 . . . . . . 7 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
346345ralrimiva 3113 . . . . . 6 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
347 fveq2 6375 . . . . . . . 8 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
348 fveq2 6375 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
349348oveq1d 6857 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
350349oveq1d 6857 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
351350sumeq2ad 14719 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
352 fveq2 6375 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
353352sumeq1d 14716 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
354351, 353eqtrd 2799 . . . . . . . . 9 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
355354mpteq2dv 4904 . . . . . . . 8 (𝑗 = 𝑘 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
356347, 355eqeq12d 2780 . . . . . . 7 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
357356cbvralv 3319 . . . . . 6 (∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
358346, 357sylib 209 . . . . 5 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
359358ex 401 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
36016, 32, 48, 68, 249, 359, 295findcard2d 8409 . . 3 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
361 nn0uz 11922 . . . . 5 0 = (ℤ‘0)
362301, 361syl6eleq 2854 . . . 4 (𝜑𝑁 ∈ (ℤ‘0))
363 eluzfz2 12556 . . . 4 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
364362, 363syl 17 . . 3 (𝜑𝑁 ∈ (0...𝑁))
365 fveq2 6375 . . . . 5 (𝑘 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑁))
366 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑁 → ((𝐷𝑇)‘𝑘) = ((𝐷𝑇)‘𝑁))
367366sumeq1d 14716 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
368 fveq2 6375 . . . . . . . . . 10 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
369368oveq1d 6857 . . . . . . . . 9 (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) = ((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
370369oveq1d 6857 . . . . . . . 8 (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
371370sumeq2ad 14719 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
372367, 371eqtrd 2799 . . . . . 6 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
373372mpteq2dv 4904 . . . . 5 (𝑘 = 𝑁 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
374365, 373eqeq12d 2780 . . . 4 (𝑘 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
375374rspccva 3460 . . 3 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
376360, 364, 375syl2anc 579 . 2 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
377 oveq2 6850 . . . . . . . . . . 11 (𝑠 = 𝑇 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇))
378 rabeq 3341 . . . . . . . . . . 11 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
379377, 378syl 17 . . . . . . . . . 10 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
380 sumeq1 14704 . . . . . . . . . . . 12 (𝑠 = 𝑇 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑇 (𝑐𝑡))
381380eqeq1d 2767 . . . . . . . . . . 11 (𝑠 = 𝑇 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑇 (𝑐𝑡) = 𝑛))
382381rabbidv 3338 . . . . . . . . . 10 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
383379, 382eqtrd 2799 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
384383mpteq2dv 4904 . . . . . . . 8 (𝑠 = 𝑇 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
385384adantl 473 . . . . . . 7 ((𝜑𝑠 = 𝑇) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
386 pwidg 4330 . . . . . . . 8 (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
387295, 386syl 17 . . . . . . 7 (𝜑𝑇 ∈ 𝒫 𝑇)
388139mptex 6679 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V
389388a1i 11 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V)
390106, 385, 387, 389fvmptd 6477 . . . . . 6 (𝜑 → (𝐷𝑇) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
391 dvnprodlem3.c . . . . . . 7 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
392391a1i 11 . . . . . 6 (𝜑𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
393390, 392eqtr4d 2802 . . . . 5 (𝜑 → (𝐷𝑇) = 𝐶)
394393fveq1d 6377 . . . 4 (𝜑 → ((𝐷𝑇)‘𝑁) = (𝐶𝑁))
395394sumeq1d 14716 . . 3 (𝜑 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
396395mpteq2dv 4904 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
397376, 396eqtrd 2799 1 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107  wal 1650   = wceq 1652  wcel 2155  wne 2937  wral 3055  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  wss 3732  c0 4079  ifcif 4243  𝒫 cpw 4315  {csn 4334  {cpr 4336  cop 4340  cmpt 4888  dom cdm 5277  cres 5279   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  pm cpm 8061  Fincfn 8160  cc 10187  cr 10188  0cc0 10189  1c1 10190   · cmul 10194  cmin 10520   / cdiv 10938  cn 11274  0cn0 11538  cuz 11886  ...cfz 12533  !cfa 13264  Σcsu 14701  cprod 14918  t crest 16347  TopOpenctopn 16348  fldccnfld 20019   D𝑛 cdvn 23919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-sum 14702  df-prod 14919  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-hom 16238  df-cco 16239  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-pt 16371  df-prds 16374  df-xrs 16428  df-qtop 16433  df-imas 16434  df-xps 16436  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-mulg 17808  df-cntz 18013  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922  df-dvn 23923
This theorem is referenced by:  dvnprod  40802
  Copyright terms: Public domain W3C validator