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

Theorem dvnprodlem3 41698
 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 15129 . . . . . . . . 9 (𝑠 = ∅ → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))
21mpteq2dv 5028 . . . . . . . 8 (𝑠 = ∅ → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))
32oveq2d 6998 . . . . . . 7 (𝑠 = ∅ → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))))
43fveq1d 6506 . . . . . 6 (𝑠 = ∅ → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘))
5 fveq2 6504 . . . . . . . . . 10 (𝑠 = ∅ → (𝐷𝑠) = (𝐷‘∅))
65fveq1d 6506 . . . . . . . . 9 (𝑠 = ∅ → ((𝐷𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
76sumeq1d 14924 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
8 prodeq1 15129 . . . . . . . . . . 11 (𝑠 = ∅ → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐𝑡)))
98oveq2d 6998 . . . . . . . . . 10 (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
10 prodeq1 15129 . . . . . . . . . 10 (𝑠 = ∅ → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
119, 10oveq12d 7000 . . . . . . . . 9 (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1211sumeq2sdv 14927 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
137, 12eqtrd 2816 . . . . . . 7 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1413mpteq2dv 5028 . . . . . 6 (𝑠 = ∅ → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
154, 14eqeq12d 2795 . . . . 5 (𝑠 = ∅ → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
1615ralbidv 3149 . . . 4 (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
17 prodeq1 15129 . . . . . . . . 9 (𝑠 = 𝑟 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))
1817mpteq2dv 5028 . . . . . . . 8 (𝑠 = 𝑟 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
1918oveq2d 6998 . . . . . . 7 (𝑠 = 𝑟 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
2019fveq1d 6506 . . . . . 6 (𝑠 = 𝑟 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘))
21 fveq2 6504 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝐷𝑠) = (𝐷𝑟))
2221fveq1d 6506 . . . . . . . . 9 (𝑠 = 𝑟 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑟)‘𝑘))
2322sumeq1d 14924 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
24 prodeq1 15129 . . . . . . . . . . 11 (𝑠 = 𝑟 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑟 (!‘(𝑐𝑡)))
2524oveq2d 6998 . . . . . . . . . 10 (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
26 prodeq1 15129 . . . . . . . . . 10 (𝑠 = 𝑟 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
2725, 26oveq12d 7000 . . . . . . . . 9 (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2827sumeq2sdv 14927 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2923, 28eqtrd 2816 . . . . . . 7 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
3029mpteq2dv 5028 . . . . . 6 (𝑠 = 𝑟 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
3120, 30eqeq12d 2795 . . . . 5 (𝑠 = 𝑟 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
3231ralbidv 3149 . . . 4 (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
33 prodeq1 15129 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))
3433mpteq2dv 5028 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))
3534oveq2d 6998 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))))
3635fveq1d 6506 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
37 fveq2 6504 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
3837fveq1d 6506 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
3938sumeq1d 14924 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
40 prodeq1 15129 . . . . . . . . . . 11 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡)))
4140oveq2d 6998 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
42 prodeq1 15129 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
4341, 42oveq12d 7000 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4443sumeq2sdv 14927 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4539, 44eqtrd 2816 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4645mpteq2dv 5028 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
4736, 46eqeq12d 2795 . . . . 5 (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
4847ralbidv 3149 . . . 4 (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
49 prodeq1 15129 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5049mpteq2dv 5028 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
51 dvnprodlem3.f . . . . . . . . . . 11 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5251a1i 11 . . . . . . . . . 10 (𝑠 = 𝑇𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
5352eqcomd 2786 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)) = 𝐹)
5450, 53eqtrd 2816 . . . . . . . 8 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = 𝐹)
5554oveq2d 6998 . . . . . . 7 (𝑠 = 𝑇 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 𝐹))
5655fveq1d 6506 . . . . . 6 (𝑠 = 𝑇 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘))
57 fveq2 6504 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝐷𝑠) = (𝐷𝑇))
5857fveq1d 6506 . . . . . . . . 9 (𝑠 = 𝑇 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑇)‘𝑘))
5958sumeq1d 14924 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
60 prodeq1 15129 . . . . . . . . . . 11 (𝑠 = 𝑇 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑇 (!‘(𝑐𝑡)))
6160oveq2d 6998 . . . . . . . . . 10 (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
62 prodeq1 15129 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
6361, 62oveq12d 7000 . . . . . . . . 9 (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6463sumeq2sdv 14927 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6559, 64eqtrd 2816 . . . . . . 7 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6665mpteq2dv 5028 . . . . . 6 (𝑠 = 𝑇 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
6756, 66eqeq12d 2795 . . . . 5 (𝑠 = 𝑇 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
6867ralbidv 3149 . . . 4 (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
69 prod0 15163 . . . . . . . . . . . . 13 𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥) = 1
7069mpteq2i 5024 . . . . . . . . . . . 12 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ 1)
7170oveq2i 6993 . . . . . . . . . . 11 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1))
7271a1i 11 . . . . . . . . . 10 (𝑘 = 0 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1)))
73 id 22 . . . . . . . . . 10 (𝑘 = 0 → 𝑘 = 0)
7472, 73fveq12d 6511 . . . . . . . . 9 (𝑘 = 0 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
7574adantl 474 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
76 dvnprodlem3.s . . . . . . . . . . 11 (𝜑𝑆 ∈ {ℝ, ℂ})
77 recnprss 24220 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
7876, 77syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
79 1cnd 10440 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 1 ∈ ℂ)
8079fmpttd 6708 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ 1):𝑋⟶ℂ)
81 1re 10445 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
8281rgenw 3102 . . . . . . . . . . . . . . . 16 𝑥𝑋 1 ∈ ℝ
83 dmmptg 5940 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 1 ∈ ℝ → dom (𝑥𝑋 ↦ 1) = 𝑋)
8482, 83ax-mp 5 . . . . . . . . . . . . . . 15 dom (𝑥𝑋 ↦ 1) = 𝑋
8584a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑥𝑋 ↦ 1) = 𝑋)
8685feq2d 6335 . . . . . . . . . . . . 13 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ↔ (𝑥𝑋 ↦ 1):𝑋⟶ℂ))
8780, 86mpbird 249 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ)
88 restsspw 16567 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆
89 dvnprodlem3.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
9088, 89sseldi 3858 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ 𝒫 𝑆)
91 elpwi 4435 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝒫 𝑆𝑋𝑆)
9290, 91syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝑆)
9385, 92eqsstrd 3897 . . . . . . . . . . . 12 (𝜑 → dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)
9487, 93jca 504 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆))
95 cnex 10422 . . . . . . . . . . . . 13 ℂ ∈ V
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
97 elpm2g 8229 . . . . . . . . . . . 12 ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9896, 76, 97syl2anc 576 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9994, 98mpbird 249 . . . . . . . . . 10 (𝜑 → (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆))
100 dvn0 24239 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
10178, 99, 100syl2anc 576 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
102101adantr 473 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
103 fveq2 6504 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
104103adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105 dvnprodlem3.d . . . . . . . . . . . . . . . . 17 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
106 oveq2 6990 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 ∅))
107 elmapfn 8235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 Fn ∅)
108 fn0 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 Fn ∅ ↔ 𝑥 = ∅)
109107, 108sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 = ∅)
110 velsn 4460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
111109, 110sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 ∈ {∅})
112110biimpi 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} → 𝑥 = ∅)
113 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → 𝑥 = ∅)
114 f0 6394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅:∅⟶(0...𝑛)
115 ovex 7014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0...𝑛) ∈ V
116 0ex 5072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ V
117115, 116elmap 8241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∅ ∈ ((0...𝑛) ↑𝑚 ∅) ↔ ∅:∅⟶(0...𝑛))
118114, 117mpbir 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ∈ ((0...𝑛) ↑𝑚 ∅)
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑𝑚 ∅))
120113, 119eqeltrd 2868 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
121112, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
122111, 121impbii 201 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
123122ax-gen 1759 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
124 dfcleq 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑛) ↑𝑚 ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅}))
125123, 124mpbir 223 . . . . . . . . . . . . . . . . . . . . . 22 ((0...𝑛) ↑𝑚 ∅) = {∅}
126125a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 ∅) = {∅})
127106, 126eqtrd 2816 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = {∅})
128 rabeq 3408 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑𝑚 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
129127, 128syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
130 sumeq1 14912 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ ∅ (𝑐𝑡))
131130eqeq1d 2782 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛))
132131rabbidv 3405 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
133129, 132eqtrd 2816 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
134133mpteq2dv 5028 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
135 0elpw 5114 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑇
136135a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ ∈ 𝒫 𝑇)
137 nn0ex 11720 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
138137mptex 6818 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V
139138a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V)
140105, 134, 136, 139fvmptd3 6623 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
141 eqeq2 2791 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0))
142141rabbidv 3405 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
143142adantl 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
144 0nn0 11730 . . . . . . . . . . . . . . . . 17 0 ∈ ℕ0
145144a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℕ0)
146 p0ex 5141 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
147146rabex 5095 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V
148147a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V)
149140, 143, 145, 148fvmptd 6607 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
150149adantr 473 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
151 snidg 4476 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ V → ∅ ∈ {∅})
152116, 151ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ {∅}
153 eqid 2780 . . . . . . . . . . . . . . . . . . . 20 0 = 0
154152, 153pm3.2i 463 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {∅} ∧ 0 = 0)
155 sum0 14944 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑡 ∈ ∅ (𝑐𝑡) = 0
156155a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
157156eqeq1d 2782 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 0 ↔ 0 = 0))
158157elrab 3597 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
159154, 158mpbir 223 . . . . . . . . . . . . . . . . . 18 ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
160159n0ii 4191 . . . . . . . . . . . . . . . . 17 ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅
161 eqid 2780 . . . . . . . . . . . . . . . . . 18 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
162 rabrsn 4539 . . . . . . . . . . . . . . . . . 18 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
164160, 163mtpor 1734 . . . . . . . . . . . . . . . 16 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}
165164a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
166 iftrue 4359 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
167166adantl 474 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
168165, 167eqtr4d 2819 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
169104, 150, 1683eqtrd 2820 . . . . . . . . . . . . 13 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
170169, 167eqtrd 2816 . . . . . . . . . . . 12 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
171170sumeq1d 14924 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
172 fveq2 6504 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘𝑘) = (!‘0))
173 fac0 13457 . . . . . . . . . . . . . . . . . . 19 (!‘0) = 1
174173a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘0) = 1)
175172, 174eqtrd 2816 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (!‘𝑘) = 1)
176175oveq1d 6997 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
177 prod0 15163 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ ∅ (!‘(𝑐𝑡)) = 1
178177oveq2i 6993 . . . . . . . . . . . . . . . . 17 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / 1)
179 1div1e1 11137 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
180178, 179eqtri 2804 . . . . . . . . . . . . . . . 16 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1
181176, 180syl6eq 2832 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1)
182 prod0 15163 . . . . . . . . . . . . . . . 16 𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1
183182a1i 11 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1)
184181, 183oveq12d 7000 . . . . . . . . . . . . . 14 (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
185184ad2antlr 715 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
186 1t1e1 11615 . . . . . . . . . . . . . 14 (1 · 1) = 1
187186a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
188185, 187eqtrd 2816 . . . . . . . . . . . 12 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
189188sumeq2dv 14926 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
190 ax-1cn 10399 . . . . . . . . . . . . 13 1 ∈ ℂ
191 eqidd 2781 . . . . . . . . . . . . . 14 (𝑐 = ∅ → 1 = 1)
192191sumsn 14967 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
193116, 190, 192mp2an 680 . . . . . . . . . . . 12 Σ𝑐 ∈ {∅}1 = 1
194193a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
195171, 189, 1943eqtrd 2820 . . . . . . . . . 10 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
196195mpteq2dv 5028 . . . . . . . . 9 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ 1))
197196eqcomd 2786 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
19875, 102, 1973eqtrd 2820 . . . . . . 7 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
199198a1d 25 . . . . . 6 ((𝜑𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
20071fveq1i 6505 . . . . . . . . 9 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘)
201200a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘))
20276adantr 473 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
203202adantr 473 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
20489adantr 473 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
205204adantr 473 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
206190a1i 11 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
207 elfznn0 12822 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
208207adantl 474 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
209 neqne 2977 . . . . . . . . . . . . 13 𝑘 = 0 → 𝑘 ≠ 0)
210209adantr 473 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
211208, 210jca 504 . . . . . . . . . . 11 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ0𝑘 ≠ 0))
212 elnnne0 11729 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
213211, 212sylibr 226 . . . . . . . . . 10 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
214213adantll 702 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
215203, 205, 206, 214dvnmptconst 41691 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘) = (𝑥𝑋 ↦ 0))
216140ad2antrr 714 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
217 eqeq2 2791 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘))
218217rabbidv 3405 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
219218adantl 474 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
220 eqidd 2781 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 𝑘)
221 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
222221eqcomd 2786 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = Σ𝑡 ∈ ∅ (𝑐𝑡))
223155a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
224220, 222, 2233eqtrd 2820 . . . . . . . . . . . . . . . . . . . . 21 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 0)
225224adantl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
226225adantll 702 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
227 simpll 755 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → ¬ 𝑘 = 0)
228226, 227pm2.65da 805 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
229228ralrimiva 3134 . . . . . . . . . . . . . . . . 17 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
230 rabeq0 4227 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
231229, 230sylibr 226 . . . . . . . . . . . . . . . 16 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
232231adantr 473 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
233219, 232eqtrd 2816 . . . . . . . . . . . . . 14 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
234233adantll 702 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
235234adantlr 703 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
236207adantl 474 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
237116a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
238216, 235, 236, 237fvmptd 6607 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
239238sumeq1d 14924 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
240 sum0 14944 . . . . . . . . . . 11 Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0
241240a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0)
242239, 241eqtr2d 2817 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
243242mpteq2dv 5028 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
244201, 215, 2433eqtrd 2820 . . . . . . 7 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
245244ex 405 . . . . . 6 ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
246199, 245pm2.61dan 801 . . . . 5 (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
247246ralrimiv 3133 . . . 4 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
248 simpll 755 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))))
249 fveq2 6504 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑡)‘𝑦))
250249prodeq2ad 41339 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑦))
251 fveq2 6504 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (𝐻𝑡) = (𝐻𝑢))
252251fveq1d 6506 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑢)‘𝑦))
253252cbvprodv 15136 . . . . . . . . . . . . . . . . 17 𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)
254253a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
255250, 254eqtrd 2816 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
256255cbvmptv 5033 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)) = (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
257256oveq2i 6993 . . . . . . . . . . . . 13 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))
258257fveq1i 6505 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘)
259 fveq2 6504 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → (𝑐𝑡) = (𝑐𝑢))
260259fveq2d 6508 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑢)))
261260cbvprodv 15136 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (!‘(𝑐𝑡)) = ∏𝑢𝑟 (!‘(𝑐𝑢))
262261oveq2i 6993 . . . . . . . . . . . . . . . . 17 ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢)))
263262a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))))
264 fveq2 6504 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
265264prodeq2ad 41339 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
266251oveq2d 6998 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑢 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑢)))
267266, 259fveq12d 6511 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)))
268267fveq1d 6506 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
269268cbvprodv 15136 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)
270269a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
271265, 270eqtrd 2816 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
272263, 271oveq12d 7000 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
273272sumeq2sdv 14927 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
274 fveq1 6503 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → (𝑐𝑢) = (𝑑𝑢))
275274fveq2d 6508 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (!‘(𝑐𝑢)) = (!‘(𝑑𝑢)))
276275prodeq2ad 41339 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → ∏𝑢𝑟 (!‘(𝑐𝑢)) = ∏𝑢𝑟 (!‘(𝑑𝑢)))
277276oveq2d 6998 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))))
278274fveq2d 6508 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢)))
279278fveq1d 6506 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
280279prodeq2ad 41339 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
281277, 280oveq12d 7000 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
282281cbvsumv 14919 . . . . . . . . . . . . . . 15 Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
283282a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
284273, 283eqtrd 2816 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
285284cbvmptv 5033 . . . . . . . . . . . 12 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
286258, 285eqeq12i 2794 . . . . . . . . . . 11 (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
287286ralbii 3117 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
288287biimpi 208 . . . . . . . . 9 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
289288ad2antlr 715 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
290 simpr 477 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
29176ad3antrrr 718 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
29289ad3antrrr 718 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
293 dvnprodlem3.t . . . . . . . . . 10 (𝜑𝑇 ∈ Fin)
294293ad3antrrr 718 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
295 simp-4l 771 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝜑)
296 simpr 477 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝑡𝑇)
297 dvnprodlem3.h . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
298295, 296, 297syl2anc 576 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
299 dvnprodlem3.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
300299ad3antrrr 718 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
301 simplll 763 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
3023013ad2ant1 1114 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝜑)
303 simp2 1118 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝑡𝑇)
304 simp3 1119 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ∈ (0...𝑁))
305 eleq1w 2850 . . . . . . . . . . . . 13 (𝑗 = → (𝑗 ∈ (0...𝑁) ↔ ∈ (0...𝑁)))
3063053anbi3d 1422 . . . . . . . . . . . 12 (𝑗 = → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∈ (0...𝑁))))
307 fveq2 6504 . . . . . . . . . . . . 13 (𝑗 = → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘))
308307feq1d 6334 . . . . . . . . . . . 12 (𝑗 = → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ))
309306, 308imbi12d 337 . . . . . . . . . . 11 (𝑗 = → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)))
310 dvnprodlem3.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
311309, 310chvarv 2328 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
312302, 303, 304, 311syl3anc 1352 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
313 simprl 759 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑟𝑇)
314313ad2antrr 714 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟𝑇)
315 simprr 761 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑧 ∈ (𝑇𝑟))
316315ad2antrr 714 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇𝑟))
317257eqcomi 2789 . . . . . . . . . . . . . . 15 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
318317a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
319 id 22 . . . . . . . . . . . . . 14 (𝑘 = 𝑙𝑘 = 𝑙)
320318, 319fveq12d 6511 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙))
321285eqcomi 2789 . . . . . . . . . . . . . . 15 (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
322321a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
323 fveq2 6504 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
324323oveq1d 6997 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
325324oveq1d 6997 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
326325sumeq2sdv 14927 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
327 fveq2 6504 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝐷𝑟)‘𝑘) = ((𝐷𝑟)‘𝑙))
328327sumeq1d 14924 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
329326, 328eqtrd 2816 . . . . . . . . . . . . . . 15 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
330329mpteq2dv 5028 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
331322, 330eqtrd 2816 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
332320, 331eqeq12d 2795 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
333332cbvralv 3385 . . . . . . . . . . 11 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
334333biimpi 208 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
335334ad2antlr 715 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
336 simpr 477 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
337 fveq1 6503 . . . . . . . . . . . 12 (𝑑 = 𝑐 → (𝑑𝑧) = (𝑐𝑧))
338337oveq2d 6998 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑗 − (𝑑𝑧)) = (𝑗 − (𝑐𝑧)))
339 reseq1 5694 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑑𝑟) = (𝑐𝑟))
340338, 339opeq12d 4690 . . . . . . . . . 10 (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩ = ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
341340cbvmptv 5033 . . . . . . . . 9 (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
342291, 292, 294, 298, 300, 312, 105, 314, 316, 335, 336, 341dvnprodlem2 41697 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
343248, 289, 290, 342syl21anc 826 . . . . . . 7 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
344343ralrimiva 3134 . . . . . 6 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
345 fveq2 6504 . . . . . . . 8 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
346 fveq2 6504 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
347346oveq1d 6997 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
348347oveq1d 6997 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
349348sumeq2sdv 14927 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
350 fveq2 6504 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
351350sumeq1d 14924 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
352349, 351eqtrd 2816 . . . . . . . . 9 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
353352mpteq2dv 5028 . . . . . . . 8 (𝑗 = 𝑘 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
354345, 353eqeq12d 2795 . . . . . . 7 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
355354cbvralv 3385 . . . . . 6 (∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
356344, 355sylib 210 . . . . 5 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
357356ex 405 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
35816, 32, 48, 68, 247, 357, 293findcard2d 8561 . . 3 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
359 nn0uz 12100 . . . . 5 0 = (ℤ‘0)
360299, 359syl6eleq 2878 . . . 4 (𝜑𝑁 ∈ (ℤ‘0))
361 eluzfz2 12737 . . . 4 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
362360, 361syl 17 . . 3 (𝜑𝑁 ∈ (0...𝑁))
363 fveq2 6504 . . . . 5 (𝑘 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑁))
364 fveq2 6504 . . . . . . . 8 (𝑘 = 𝑁 → ((𝐷𝑇)‘𝑘) = ((𝐷𝑇)‘𝑁))
365364sumeq1d 14924 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
366 fveq2 6504 . . . . . . . . . 10 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
367366oveq1d 6997 . . . . . . . . 9 (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) = ((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
368367oveq1d 6997 . . . . . . . 8 (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
369368sumeq2sdv 14927 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
370365, 369eqtrd 2816 . . . . . 6 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
371370mpteq2dv 5028 . . . . 5 (𝑘 = 𝑁 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
372363, 371eqeq12d 2795 . . . 4 (𝑘 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
373372rspccva 3536 . . 3 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
374358, 362, 373syl2anc 576 . 2 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
375 oveq2 6990 . . . . . . . . . 10 (𝑠 = 𝑇 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇))
376 rabeq 3408 . . . . . . . . . 10 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
377375, 376syl 17 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
378 sumeq1 14912 . . . . . . . . . . 11 (𝑠 = 𝑇 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑇 (𝑐𝑡))
379378eqeq1d 2782 . . . . . . . . . 10 (𝑠 = 𝑇 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑇 (𝑐𝑡) = 𝑛))
380379rabbidv 3405 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
381377, 380eqtrd 2816 . . . . . . . 8 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
382381mpteq2dv 5028 . . . . . . 7 (𝑠 = 𝑇 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
383 pwidg 4440 . . . . . . . 8 (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
384293, 383syl 17 . . . . . . 7 (𝜑𝑇 ∈ 𝒫 𝑇)
385137mptex 6818 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V
386385a1i 11 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V)
387105, 382, 384, 386fvmptd3 6623 . . . . . 6 (𝜑 → (𝐷𝑇) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
388 dvnprodlem3.c . . . . . . 7 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
389388a1i 11 . . . . . 6 (𝜑𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
390387, 389eqtr4d 2819 . . . . 5 (𝜑 → (𝐷𝑇) = 𝐶)
391390fveq1d 6506 . . . 4 (𝜑 → ((𝐷𝑇)‘𝑁) = (𝐶𝑁))
392391sumeq1d 14924 . . 3 (𝜑 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
393392mpteq2dv 5028 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
394374, 393eqtrd 2816 1 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 834   ∧ w3a 1069  ∀wal 1506   = wceq 1508   ∈ wcel 2051   ≠ wne 2969  ∀wral 3090  {crab 3094  Vcvv 3417   ∖ cdif 3828   ∪ cun 3829   ⊆ wss 3831  ∅c0 4181  ifcif 4353  𝒫 cpw 4425  {csn 4444  {cpr 4446  ⟨cop 4450   ↦ cmpt 5013  dom cdm 5411   ↾ cres 5413   Fn wfn 6188  ⟶wf 6189  ‘cfv 6193  (class class class)co 6982   ↑𝑚 cmap 8212   ↑pm cpm 8213  Fincfn 8312  ℂcc 10339  ℝcr 10340  0cc0 10341  1c1 10342   · cmul 10346   − cmin 10676   / cdiv 11104  ℕcn 11445  ℕ0cn0 11713  ℤ≥cuz 12064  ...cfz 12714  !cfa 13454  Σcsu 14909  ∏cprod 15125   ↾t crest 16556  TopOpenctopn 16557  ℂfldccnfld 20262   D𝑛 cdvn 24180 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285  ax-inf2 8904  ax-cnex 10397  ax-resscn 10398  ax-1cn 10399  ax-icn 10400  ax-addcl 10401  ax-addrcl 10402  ax-mulcl 10403  ax-mulrcl 10404  ax-mulcom 10405  ax-addass 10406  ax-mulass 10407  ax-distr 10408  ax-i2m1 10409  ax-1ne0 10410  ax-1rid 10411  ax-rnegex 10412  ax-rrecex 10413  ax-cnre 10414  ax-pre-lttri 10415  ax-pre-lttrn 10416  ax-pre-ltadd 10417  ax-pre-mulgt0 10418  ax-pre-sup 10419  ax-addf 10420  ax-mulf 10421 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-tp 4449  df-op 4451  df-uni 4718  df-int 4755  df-iun 4799  df-iin 4800  df-br 4935  df-opab 4997  df-mpt 5014  df-tr 5036  df-id 5316  df-eprel 5321  df-po 5330  df-so 5331  df-fr 5370  df-se 5371  df-we 5372  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-pred 5991  df-ord 6037  df-on 6038  df-lim 6039  df-suc 6040  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-isom 6202  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-of 7233  df-om 7403  df-1st 7507  df-2nd 7508  df-supp 7640  df-wrecs 7756  df-recs 7818  df-rdg 7856  df-1o 7911  df-2o 7912  df-oadd 7915  df-er 8095  df-map 8214  df-pm 8215  df-ixp 8266  df-en 8313  df-dom 8314  df-sdom 8315  df-fin 8316  df-fsupp 8635  df-fi 8676  df-sup 8707  df-inf 8708  df-oi 8775  df-card 9168  df-cda 9394  df-pnf 10482  df-mnf 10483  df-xr 10484  df-ltxr 10485  df-le 10486  df-sub 10678  df-neg 10679  df-div 11105  df-nn 11446  df-2 11509  df-3 11510  df-4 11511  df-5 11512  df-6 11513  df-7 11514  df-8 11515  df-9 11516  df-n0 11714  df-z 11800  df-dec 11918  df-uz 12065  df-q 12169  df-rp 12211  df-xneg 12330  df-xadd 12331  df-xmul 12332  df-ico 12566  df-icc 12567  df-fz 12715  df-fzo 12856  df-seq 13191  df-exp 13251  df-fac 13455  df-bc 13484  df-hash 13512  df-cj 14325  df-re 14326  df-im 14327  df-sqrt 14461  df-abs 14462  df-clim 14712  df-sum 14910  df-prod 15126  df-struct 16347  df-ndx 16348  df-slot 16349  df-base 16351  df-sets 16352  df-ress 16353  df-plusg 16440  df-mulr 16441  df-starv 16442  df-sca 16443  df-vsca 16444  df-ip 16445  df-tset 16446  df-ple 16447  df-ds 16449  df-unif 16450  df-hom 16451  df-cco 16452  df-rest 16558  df-topn 16559  df-0g 16577  df-gsum 16578  df-topgen 16579  df-pt 16580  df-prds 16583  df-xrs 16637  df-qtop 16642  df-imas 16643  df-xps 16645  df-mre 16727  df-mrc 16728  df-acs 16730  df-mgm 17722  df-sgrp 17764  df-mnd 17775  df-submnd 17816  df-mulg 18024  df-cntz 18230  df-cmn 18680  df-psmet 20254  df-xmet 20255  df-met 20256  df-bl 20257  df-mopn 20258  df-fbas 20259  df-fg 20260  df-cnfld 20263  df-top 21221  df-topon 21238  df-topsp 21260  df-bases 21273  df-cld 21346  df-ntr 21347  df-cls 21348  df-nei 21425  df-lp 21463  df-perf 21464  df-cn 21554  df-cnp 21555  df-haus 21642  df-tx 21889  df-hmeo 22082  df-fil 22173  df-fm 22265  df-flim 22266  df-flf 22267  df-xms 22648  df-ms 22649  df-tms 22650  df-cncf 23204  df-limc 24182  df-dv 24183  df-dvn 24184 This theorem is referenced by:  dvnprod  41699
 Copyright terms: Public domain W3C validator