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 42583
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...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
dvnprodlem3.c 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
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 15259 . . . . . . . . 9 (𝑠 = ∅ → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))
21mpteq2dv 5129 . . . . . . . 8 (𝑠 = ∅ → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))
32oveq2d 7155 . . . . . . 7 (𝑠 = ∅ → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))))
43fveq1d 6651 . . . . . 6 (𝑠 = ∅ → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘))
5 fveq2 6649 . . . . . . . . . 10 (𝑠 = ∅ → (𝐷𝑠) = (𝐷‘∅))
65fveq1d 6651 . . . . . . . . 9 (𝑠 = ∅ → ((𝐷𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
76sumeq1d 15054 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
8 prodeq1 15259 . . . . . . . . . . 11 (𝑠 = ∅ → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐𝑡)))
98oveq2d 7155 . . . . . . . . . 10 (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
10 prodeq1 15259 . . . . . . . . . 10 (𝑠 = ∅ → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
119, 10oveq12d 7157 . . . . . . . . 9 (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1211sumeq2sdv 15057 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
137, 12eqtrd 2836 . . . . . . 7 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1413mpteq2dv 5129 . . . . . 6 (𝑠 = ∅ → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
154, 14eqeq12d 2817 . . . . 5 (𝑠 = ∅ → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
1615ralbidv 3165 . . . 4 (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
17 prodeq1 15259 . . . . . . . . 9 (𝑠 = 𝑟 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))
1817mpteq2dv 5129 . . . . . . . 8 (𝑠 = 𝑟 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
1918oveq2d 7155 . . . . . . 7 (𝑠 = 𝑟 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
2019fveq1d 6651 . . . . . 6 (𝑠 = 𝑟 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘))
21 fveq2 6649 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝐷𝑠) = (𝐷𝑟))
2221fveq1d 6651 . . . . . . . . 9 (𝑠 = 𝑟 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑟)‘𝑘))
2322sumeq1d 15054 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
24 prodeq1 15259 . . . . . . . . . . 11 (𝑠 = 𝑟 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑟 (!‘(𝑐𝑡)))
2524oveq2d 7155 . . . . . . . . . 10 (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
26 prodeq1 15259 . . . . . . . . . 10 (𝑠 = 𝑟 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
2725, 26oveq12d 7157 . . . . . . . . 9 (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2827sumeq2sdv 15057 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2923, 28eqtrd 2836 . . . . . . 7 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
3029mpteq2dv 5129 . . . . . 6 (𝑠 = 𝑟 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
3120, 30eqeq12d 2817 . . . . 5 (𝑠 = 𝑟 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
3231ralbidv 3165 . . . 4 (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
33 prodeq1 15259 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))
3433mpteq2dv 5129 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))
3534oveq2d 7155 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))))
3635fveq1d 6651 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
37 fveq2 6649 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
3837fveq1d 6651 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
3938sumeq1d 15054 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
40 prodeq1 15259 . . . . . . . . . . 11 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡)))
4140oveq2d 7155 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
42 prodeq1 15259 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
4341, 42oveq12d 7157 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4443sumeq2sdv 15057 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4539, 44eqtrd 2836 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4645mpteq2dv 5129 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
4736, 46eqeq12d 2817 . . . . 5 (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
4847ralbidv 3165 . . . 4 (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
49 prodeq1 15259 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5049mpteq2dv 5129 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
51 dvnprodlem3.f . . . . . . . . . . 11 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5251a1i 11 . . . . . . . . . 10 (𝑠 = 𝑇𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
5352eqcomd 2807 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)) = 𝐹)
5450, 53eqtrd 2836 . . . . . . . 8 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = 𝐹)
5554oveq2d 7155 . . . . . . 7 (𝑠 = 𝑇 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 𝐹))
5655fveq1d 6651 . . . . . 6 (𝑠 = 𝑇 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘))
57 fveq2 6649 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝐷𝑠) = (𝐷𝑇))
5857fveq1d 6651 . . . . . . . . 9 (𝑠 = 𝑇 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑇)‘𝑘))
5958sumeq1d 15054 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
60 prodeq1 15259 . . . . . . . . . . 11 (𝑠 = 𝑇 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑇 (!‘(𝑐𝑡)))
6160oveq2d 7155 . . . . . . . . . 10 (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
62 prodeq1 15259 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
6361, 62oveq12d 7157 . . . . . . . . 9 (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6463sumeq2sdv 15057 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6559, 64eqtrd 2836 . . . . . . 7 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6665mpteq2dv 5129 . . . . . 6 (𝑠 = 𝑇 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
6756, 66eqeq12d 2817 . . . . 5 (𝑠 = 𝑇 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
6867ralbidv 3165 . . . 4 (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
69 prod0 15293 . . . . . . . . . . . . 13 𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥) = 1
7069mpteq2i 5125 . . . . . . . . . . . 12 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ 1)
7170oveq2i 7150 . . . . . . . . . . 11 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1))
7271a1i 11 . . . . . . . . . 10 (𝑘 = 0 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1)))
73 id 22 . . . . . . . . . 10 (𝑘 = 0 → 𝑘 = 0)
7472, 73fveq12d 6656 . . . . . . . . 9 (𝑘 = 0 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
7574adantl 485 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
76 dvnprodlem3.s . . . . . . . . . . 11 (𝜑𝑆 ∈ {ℝ, ℂ})
77 recnprss 24511 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
7876, 77syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
79 1cnd 10629 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 1 ∈ ℂ)
8079fmpttd 6860 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ 1):𝑋⟶ℂ)
81 1re 10634 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
8281rgenw 3121 . . . . . . . . . . . . . . . 16 𝑥𝑋 1 ∈ ℝ
83 dmmptg 6067 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 1 ∈ ℝ → dom (𝑥𝑋 ↦ 1) = 𝑋)
8482, 83ax-mp 5 . . . . . . . . . . . . . . 15 dom (𝑥𝑋 ↦ 1) = 𝑋
8584a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑥𝑋 ↦ 1) = 𝑋)
8685feq2d 6477 . . . . . . . . . . . . 13 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ↔ (𝑥𝑋 ↦ 1):𝑋⟶ℂ))
8780, 86mpbird 260 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ)
88 restsspw 16701 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆
89 dvnprodlem3.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
9088, 89sseldi 3916 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ 𝒫 𝑆)
91 elpwi 4509 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝒫 𝑆𝑋𝑆)
9290, 91syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝑆)
9385, 92eqsstrd 3956 . . . . . . . . . . . 12 (𝜑 → dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)
9487, 93jca 515 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆))
95 cnex 10611 . . . . . . . . . . . . 13 ℂ ∈ V
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
97 elpm2g 8410 . . . . . . . . . . . 12 ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9896, 76, 97syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9994, 98mpbird 260 . . . . . . . . . 10 (𝜑 → (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆))
100 dvn0 24531 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
10178, 99, 100syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
102101adantr 484 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
103 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
104103adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105 dvnprodlem3.d . . . . . . . . . . . . . . . . 17 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
106 oveq2 7147 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m ∅))
107 elmapfn 8416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 Fn ∅)
108 fn0 6455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 Fn ∅ ↔ 𝑥 = ∅)
109107, 108sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 = ∅)
110 velsn 4544 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
111109, 110sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 ∈ {∅})
112110biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} → 𝑥 = ∅)
113 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → 𝑥 = ∅)
114 f0 6538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅:∅⟶(0...𝑛)
115 ovex 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0...𝑛) ∈ V
116 0ex 5178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ V
117115, 116elmap 8422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∅ ∈ ((0...𝑛) ↑m ∅) ↔ ∅:∅⟶(0...𝑛))
118114, 117mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ∈ ((0...𝑛) ↑m ∅)
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑m ∅))
120113, 119eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑m ∅))
121112, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑m ∅))
122111, 121impbii 212 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅})
123122ax-gen 1797 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅})
124 dfcleq 2795 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑛) ↑m ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅}))
125123, 124mpbir 234 . . . . . . . . . . . . . . . . . . . . . 22 ((0...𝑛) ↑m ∅) = {∅}
126125a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑m ∅) = {∅})
127106, 126eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → ((0...𝑛) ↑m 𝑠) = {∅})
128 rabeq 3434 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑m 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
129127, 128syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
130 sumeq1 15041 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ ∅ (𝑐𝑡))
131130eqeq1d 2803 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛))
132131rabbidv 3430 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
133129, 132eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
134133mpteq2dv 5129 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
135 0elpw 5224 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑇
136135a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ ∈ 𝒫 𝑇)
137 nn0ex 11895 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
138137mptex 6967 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V
139138a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V)
140105, 134, 136, 139fvmptd3 6772 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
141 eqeq2 2813 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0))
142141rabbidv 3430 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
143142adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
144 0nn0 11904 . . . . . . . . . . . . . . . . 17 0 ∈ ℕ0
145144a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℕ0)
146 p0ex 5253 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
147146rabex 5202 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V
148147a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V)
149140, 143, 145, 148fvmptd 6756 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
150149adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
151 snidg 4562 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ V → ∅ ∈ {∅})
152116, 151ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ {∅}
153 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 0 = 0
154152, 153pm3.2i 474 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {∅} ∧ 0 = 0)
155 sum0 15074 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑡 ∈ ∅ (𝑐𝑡) = 0
156155a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
157156eqeq1d 2803 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 0 ↔ 0 = 0))
158157elrab 3631 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
159154, 158mpbir 234 . . . . . . . . . . . . . . . . . 18 ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
160159n0ii 4255 . . . . . . . . . . . . . . . . 17 ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅
161 eqid 2801 . . . . . . . . . . . . . . . . . 18 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
162 rabrsn 4623 . . . . . . . . . . . . . . . . . 18 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
164160, 163mtpor 1772 . . . . . . . . . . . . . . . 16 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}
165164a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
166 iftrue 4434 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
167166adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
168165, 167eqtr4d 2839 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
169104, 150, 1683eqtrd 2840 . . . . . . . . . . . . 13 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
170169, 167eqtrd 2836 . . . . . . . . . . . 12 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
171170sumeq1d 15054 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
172 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘𝑘) = (!‘0))
173 fac0 13636 . . . . . . . . . . . . . . . . . . 19 (!‘0) = 1
174173a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘0) = 1)
175172, 174eqtrd 2836 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (!‘𝑘) = 1)
176175oveq1d 7154 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
177 prod0 15293 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ ∅ (!‘(𝑐𝑡)) = 1
178177oveq2i 7150 . . . . . . . . . . . . . . . . 17 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / 1)
179 1div1e1 11323 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
180178, 179eqtri 2824 . . . . . . . . . . . . . . . 16 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1
181176, 180eqtrdi 2852 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1)
182 prod0 15293 . . . . . . . . . . . . . . . 16 𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1
183182a1i 11 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1)
184181, 183oveq12d 7157 . . . . . . . . . . . . . 14 (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
185184ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
186 1t1e1 11791 . . . . . . . . . . . . . 14 (1 · 1) = 1
187186a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
188185, 187eqtrd 2836 . . . . . . . . . . . 12 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
189188sumeq2dv 15056 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
190 ax-1cn 10588 . . . . . . . . . . . . 13 1 ∈ ℂ
191 eqidd 2802 . . . . . . . . . . . . . 14 (𝑐 = ∅ → 1 = 1)
192191sumsn 15097 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
193116, 190, 192mp2an 691 . . . . . . . . . . . 12 Σ𝑐 ∈ {∅}1 = 1
194193a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
195171, 189, 1943eqtrd 2840 . . . . . . . . . 10 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
196195mpteq2dv 5129 . . . . . . . . 9 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ 1))
197196eqcomd 2807 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
19875, 102, 1973eqtrd 2840 . . . . . . 7 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
199198a1d 25 . . . . . 6 ((𝜑𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
20071fveq1i 6650 . . . . . . . . 9 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘)
201200a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘))
20276adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
203202adantr 484 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
20489adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
205204adantr 484 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
206190a1i 11 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
207 elfznn0 12999 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
208207adantl 485 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
209 neqne 2998 . . . . . . . . . . . . 13 𝑘 = 0 → 𝑘 ≠ 0)
210209adantr 484 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
211208, 210jca 515 . . . . . . . . . . 11 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ0𝑘 ≠ 0))
212 elnnne0 11903 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
213211, 212sylibr 237 . . . . . . . . . 10 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
214213adantll 713 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
215203, 205, 206, 214dvnmptconst 42576 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘) = (𝑥𝑋 ↦ 0))
216140ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
217 eqeq2 2813 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘))
218217rabbidv 3430 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
219218adantl 485 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
220 eqidd 2802 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 𝑘)
221 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
222221eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = Σ𝑡 ∈ ∅ (𝑐𝑡))
223155a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
224220, 222, 2233eqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 0)
225224adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
226225adantll 713 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
227 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → ¬ 𝑘 = 0)
228226, 227pm2.65da 816 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
229228ralrimiva 3152 . . . . . . . . . . . . . . . . 17 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
230 rabeq0 4295 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
231229, 230sylibr 237 . . . . . . . . . . . . . . . 16 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
232231adantr 484 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
233219, 232eqtrd 2836 . . . . . . . . . . . . . 14 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
234233adantll 713 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
235234adantlr 714 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
236207adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
237116a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
238216, 235, 236, 237fvmptd 6756 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
239238sumeq1d 15054 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
240 sum0 15074 . . . . . . . . . . 11 Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0
241240a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0)
242239, 241eqtr2d 2837 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
243242mpteq2dv 5129 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
244201, 215, 2433eqtrd 2840 . . . . . . 7 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
245244ex 416 . . . . . 6 ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
246199, 245pm2.61dan 812 . . . . 5 (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
247246ralrimiv 3151 . . . 4 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
248 simpll 766 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))))
249 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑡)‘𝑦))
250249prodeq2ad 42227 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑦))
251 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (𝐻𝑡) = (𝐻𝑢))
252251fveq1d 6651 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑢)‘𝑦))
253252cbvprodv 15266 . . . . . . . . . . . . . . . . 17 𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)
254253a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
255250, 254eqtrd 2836 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
256255cbvmptv 5136 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)) = (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
257256oveq2i 7150 . . . . . . . . . . . . 13 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))
258257fveq1i 6650 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘)
259 fveq2 6649 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → (𝑐𝑡) = (𝑐𝑢))
260259fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑢)))
261260cbvprodv 15266 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (!‘(𝑐𝑡)) = ∏𝑢𝑟 (!‘(𝑐𝑢))
262261oveq2i 7150 . . . . . . . . . . . . . . . . 17 ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢)))
263262a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))))
264 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
265264prodeq2ad 42227 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
266251oveq2d 7155 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑢 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑢)))
267266, 259fveq12d 6656 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)))
268267fveq1d 6651 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
269268cbvprodv 15266 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)
270269a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
271265, 270eqtrd 2836 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
272263, 271oveq12d 7157 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
273272sumeq2sdv 15057 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
274 fveq1 6648 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → (𝑐𝑢) = (𝑑𝑢))
275274fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (!‘(𝑐𝑢)) = (!‘(𝑑𝑢)))
276275prodeq2ad 42227 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → ∏𝑢𝑟 (!‘(𝑐𝑢)) = ∏𝑢𝑟 (!‘(𝑑𝑢)))
277276oveq2d 7155 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))))
278274fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢)))
279278fveq1d 6651 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
280279prodeq2ad 42227 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
281277, 280oveq12d 7157 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
282281cbvsumv 15049 . . . . . . . . . . . . . . 15 Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
283282a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
284273, 283eqtrd 2836 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
285284cbvmptv 5136 . . . . . . . . . . . 12 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
286258, 285eqeq12i 2816 . . . . . . . . . . 11 (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
287286ralbii 3136 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
288287biimpi 219 . . . . . . . . 9 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
289288ad2antlr 726 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
290 simpr 488 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
29176ad3antrrr 729 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
29289ad3antrrr 729 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
293 dvnprodlem3.t . . . . . . . . . 10 (𝜑𝑇 ∈ Fin)
294293ad3antrrr 729 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
295 simp-4l 782 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝜑)
296 simpr 488 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝑡𝑇)
297 dvnprodlem3.h . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
298295, 296, 297syl2anc 587 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
299 dvnprodlem3.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
300299ad3antrrr 729 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
301 simplll 774 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
3023013ad2ant1 1130 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝜑)
303 simp2 1134 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝑡𝑇)
304 simp3 1135 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ∈ (0...𝑁))
305 eleq1w 2875 . . . . . . . . . . . . 13 (𝑗 = → (𝑗 ∈ (0...𝑁) ↔ ∈ (0...𝑁)))
3063053anbi3d 1439 . . . . . . . . . . . 12 (𝑗 = → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∈ (0...𝑁))))
307 fveq2 6649 . . . . . . . . . . . . 13 (𝑗 = → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘))
308307feq1d 6476 . . . . . . . . . . . 12 (𝑗 = → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ))
309306, 308imbi12d 348 . . . . . . . . . . 11 (𝑗 = → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)))
310 dvnprodlem3.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
311309, 310chvarvv 2005 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
312302, 303, 304, 311syl3anc 1368 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
313 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑟𝑇)
314313ad2antrr 725 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟𝑇)
315 simprr 772 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑧 ∈ (𝑇𝑟))
316315ad2antrr 725 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇𝑟))
317257eqcomi 2810 . . . . . . . . . . . . . . 15 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
318317a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
319 id 22 . . . . . . . . . . . . . 14 (𝑘 = 𝑙𝑘 = 𝑙)
320318, 319fveq12d 6656 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙))
321285eqcomi 2810 . . . . . . . . . . . . . . 15 (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
322321a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
323 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
324323oveq1d 7154 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
325324oveq1d 7154 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
326325sumeq2sdv 15057 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
327 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝐷𝑟)‘𝑘) = ((𝐷𝑟)‘𝑙))
328327sumeq1d 15054 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
329326, 328eqtrd 2836 . . . . . . . . . . . . . . 15 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
330329mpteq2dv 5129 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
331322, 330eqtrd 2836 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
332320, 331eqeq12d 2817 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
333332cbvralvw 3399 . . . . . . . . . . 11 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
334333biimpi 219 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
335334ad2antlr 726 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
336 simpr 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
337 fveq1 6648 . . . . . . . . . . . 12 (𝑑 = 𝑐 → (𝑑𝑧) = (𝑐𝑧))
338337oveq2d 7155 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑗 − (𝑑𝑧)) = (𝑗 − (𝑐𝑧)))
339 reseq1 5816 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑑𝑟) = (𝑐𝑟))
340338, 339opeq12d 4776 . . . . . . . . . 10 (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩ = ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
341340cbvmptv 5136 . . . . . . . . 9 (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
342291, 292, 294, 298, 300, 312, 105, 314, 316, 335, 336, 341dvnprodlem2 42582 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
343248, 289, 290, 342syl21anc 836 . . . . . . 7 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
344343ralrimiva 3152 . . . . . 6 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
345 fveq2 6649 . . . . . . . 8 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
346 fveq2 6649 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
347346oveq1d 7154 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
348347oveq1d 7154 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
349348sumeq2sdv 15057 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
350 fveq2 6649 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
351350sumeq1d 15054 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
352349, 351eqtrd 2836 . . . . . . . . 9 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
353352mpteq2dv 5129 . . . . . . . 8 (𝑗 = 𝑘 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
354345, 353eqeq12d 2817 . . . . . . 7 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
355354cbvralvw 3399 . . . . . 6 (∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
356344, 355sylib 221 . . . . 5 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
357356ex 416 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
35816, 32, 48, 68, 247, 357, 293findcard2d 8748 . . 3 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
359 nn0uz 12272 . . . . 5 0 = (ℤ‘0)
360299, 359eleqtrdi 2903 . . . 4 (𝜑𝑁 ∈ (ℤ‘0))
361 eluzfz2 12914 . . . 4 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
362360, 361syl 17 . . 3 (𝜑𝑁 ∈ (0...𝑁))
363 fveq2 6649 . . . . 5 (𝑘 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑁))
364 fveq2 6649 . . . . . . . 8 (𝑘 = 𝑁 → ((𝐷𝑇)‘𝑘) = ((𝐷𝑇)‘𝑁))
365364sumeq1d 15054 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
366 fveq2 6649 . . . . . . . . . 10 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
367366oveq1d 7154 . . . . . . . . 9 (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) = ((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
368367oveq1d 7154 . . . . . . . 8 (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
369368sumeq2sdv 15057 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
370365, 369eqtrd 2836 . . . . . 6 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
371370mpteq2dv 5129 . . . . 5 (𝑘 = 𝑁 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
372363, 371eqeq12d 2817 . . . 4 (𝑘 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
373372rspccva 3573 . . 3 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
374358, 362, 373syl2anc 587 . 2 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
375 oveq2 7147 . . . . . . . . . 10 (𝑠 = 𝑇 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑇))
376 rabeq 3434 . . . . . . . . . 10 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑇) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
377375, 376syl 17 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
378 sumeq1 15041 . . . . . . . . . . 11 (𝑠 = 𝑇 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑇 (𝑐𝑡))
379378eqeq1d 2803 . . . . . . . . . 10 (𝑠 = 𝑇 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑇 (𝑐𝑡) = 𝑛))
380379rabbidv 3430 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
381377, 380eqtrd 2836 . . . . . . . 8 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
382381mpteq2dv 5129 . . . . . . 7 (𝑠 = 𝑇 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
383 pwidg 4522 . . . . . . . 8 (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
384293, 383syl 17 . . . . . . 7 (𝜑𝑇 ∈ 𝒫 𝑇)
385137mptex 6967 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V
386385a1i 11 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V)
387105, 382, 384, 386fvmptd3 6772 . . . . . 6 (𝜑 → (𝐷𝑇) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
388 dvnprodlem3.c . . . . . . 7 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
389388a1i 11 . . . . . 6 (𝜑𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
390387, 389eqtr4d 2839 . . . . 5 (𝜑 → (𝐷𝑇) = 𝐶)
391390fveq1d 6651 . . . 4 (𝜑 → ((𝐷𝑇)‘𝑁) = (𝐶𝑁))
392391sumeq1d 15054 . . 3 (𝜑 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
393392mpteq2dv 5129 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
394374, 393eqtrd 2836 1 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084  wal 1536   = wceq 1538  wcel 2112  wne 2990  wral 3109  {crab 3113  Vcvv 3444  cdif 3881  cun 3882  wss 3884  c0 4246  ifcif 4428  𝒫 cpw 4500  {csn 4528  {cpr 4530  cop 4534  cmpt 5113  dom cdm 5523  cres 5525   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  m cmap 8393  pm cpm 8394  Fincfn 8496  cc 10528  cr 10529  0cc0 10530  1c1 10531   · cmul 10535  cmin 10863   / cdiv 11290  cn 11629  0cn0 11889  cuz 12235  ...cfz 12889  !cfa 13633  Σcsu 15038  cprod 15255  t crest 16690  TopOpenctopn 16691  fldccnfld 20095   D𝑛 cdvn 24471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-fac 13634  df-bc 13663  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-sum 15039  df-prod 15256  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cld 21628  df-ntr 21629  df-cls 21630  df-nei 21707  df-lp 21745  df-perf 21746  df-cn 21836  df-cnp 21837  df-haus 21924  df-tx 22171  df-hmeo 22364  df-fil 22455  df-fm 22547  df-flim 22548  df-flf 22549  df-xms 22931  df-ms 22932  df-tms 22933  df-cncf 23487  df-limc 24473  df-dv 24474  df-dvn 24475
This theorem is referenced by:  dvnprod  42584
  Copyright terms: Public domain W3C validator