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 38662
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 14427 . . . . . . . . 9 (𝑠 = ∅ → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))
21mpteq2dv 4667 . . . . . . . 8 (𝑠 = ∅ → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))
32oveq2d 6543 . . . . . . 7 (𝑠 = ∅ → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))))
43fveq1d 6090 . . . . . 6 (𝑠 = ∅ → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘))
5 fveq2 6088 . . . . . . . . . 10 (𝑠 = ∅ → (𝐷𝑠) = (𝐷‘∅))
65fveq1d 6090 . . . . . . . . 9 (𝑠 = ∅ → ((𝐷𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
76sumeq1d 14228 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
8 prodeq1 14427 . . . . . . . . . . 11 (𝑠 = ∅ → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐𝑡)))
98oveq2d 6543 . . . . . . . . . 10 (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
10 prodeq1 14427 . . . . . . . . . 10 (𝑠 = ∅ → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
119, 10oveq12d 6545 . . . . . . . . 9 (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1211sumeq2ad 38456 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
137, 12eqtrd 2643 . . . . . . 7 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1413mpteq2dv 4667 . . . . . 6 (𝑠 = ∅ → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
154, 14eqeq12d 2624 . . . . 5 (𝑠 = ∅ → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
1615ralbidv 2968 . . . 4 (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
17 prodeq1 14427 . . . . . . . . 9 (𝑠 = 𝑟 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))
1817mpteq2dv 4667 . . . . . . . 8 (𝑠 = 𝑟 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
1918oveq2d 6543 . . . . . . 7 (𝑠 = 𝑟 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
2019fveq1d 6090 . . . . . 6 (𝑠 = 𝑟 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘))
21 fveq2 6088 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝐷𝑠) = (𝐷𝑟))
2221fveq1d 6090 . . . . . . . . 9 (𝑠 = 𝑟 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑟)‘𝑘))
2322sumeq1d 14228 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
24 prodeq1 14427 . . . . . . . . . . 11 (𝑠 = 𝑟 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑟 (!‘(𝑐𝑡)))
2524oveq2d 6543 . . . . . . . . . 10 (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
26 prodeq1 14427 . . . . . . . . . 10 (𝑠 = 𝑟 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
2725, 26oveq12d 6545 . . . . . . . . 9 (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2827sumeq2ad 38456 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2923, 28eqtrd 2643 . . . . . . 7 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
3029mpteq2dv 4667 . . . . . 6 (𝑠 = 𝑟 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
3120, 30eqeq12d 2624 . . . . 5 (𝑠 = 𝑟 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
3231ralbidv 2968 . . . 4 (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
33 prodeq1 14427 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))
3433mpteq2dv 4667 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))
3534oveq2d 6543 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))))
3635fveq1d 6090 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
37 fveq2 6088 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
3837fveq1d 6090 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
3938sumeq1d 14228 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
40 prodeq1 14427 . . . . . . . . . . 11 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡)))
4140oveq2d 6543 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
42 prodeq1 14427 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
4341, 42oveq12d 6545 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4443sumeq2ad 38456 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4539, 44eqtrd 2643 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4645mpteq2dv 4667 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
4736, 46eqeq12d 2624 . . . . 5 (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
4847ralbidv 2968 . . . 4 (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
49 prodeq1 14427 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5049mpteq2dv 4667 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
51 dvnprodlem3.f . . . . . . . . . . 11 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5251a1i 11 . . . . . . . . . 10 (𝑠 = 𝑇𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
5352eqcomd 2615 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)) = 𝐹)
5450, 53eqtrd 2643 . . . . . . . 8 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = 𝐹)
5554oveq2d 6543 . . . . . . 7 (𝑠 = 𝑇 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 𝐹))
5655fveq1d 6090 . . . . . 6 (𝑠 = 𝑇 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘))
57 fveq2 6088 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝐷𝑠) = (𝐷𝑇))
5857fveq1d 6090 . . . . . . . . 9 (𝑠 = 𝑇 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑇)‘𝑘))
5958sumeq1d 14228 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
60 prodeq1 14427 . . . . . . . . . . 11 (𝑠 = 𝑇 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑇 (!‘(𝑐𝑡)))
6160oveq2d 6543 . . . . . . . . . 10 (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
62 prodeq1 14427 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
6361, 62oveq12d 6545 . . . . . . . . 9 (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6463sumeq2ad 38456 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6559, 64eqtrd 2643 . . . . . . 7 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6665mpteq2dv 4667 . . . . . 6 (𝑠 = 𝑇 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
6756, 66eqeq12d 2624 . . . . 5 (𝑠 = 𝑇 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
6867ralbidv 2968 . . . 4 (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
69 prod0 14461 . . . . . . . . . . . . 13 𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥) = 1
7069mpteq2i 4663 . . . . . . . . . . . 12 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ 1)
7170oveq2i 6538 . . . . . . . . . . 11 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1))
7271a1i 11 . . . . . . . . . 10 (𝑘 = 0 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1)))
73 id 22 . . . . . . . . . 10 (𝑘 = 0 → 𝑘 = 0)
7472, 73fveq12d 6094 . . . . . . . . 9 (𝑘 = 0 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
7574adantl 480 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
76 dvnprodlem3.s . . . . . . . . . . 11 (𝜑𝑆 ∈ {ℝ, ℂ})
77 recnprss 23419 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
7876, 77syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
79 1cnd 9913 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 1 ∈ ℂ)
80 eqid 2609 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ 1)
8179, 80fmptd 6277 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ 1):𝑋⟶ℂ)
82 1re 9896 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
8382rgenw 2907 . . . . . . . . . . . . . . . 16 𝑥𝑋 1 ∈ ℝ
84 dmmptg 5535 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 1 ∈ ℝ → dom (𝑥𝑋 ↦ 1) = 𝑋)
8583, 84ax-mp 5 . . . . . . . . . . . . . . 15 dom (𝑥𝑋 ↦ 1) = 𝑋
8685a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑥𝑋 ↦ 1) = 𝑋)
8786feq2d 5930 . . . . . . . . . . . . 13 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ↔ (𝑥𝑋 ↦ 1):𝑋⟶ℂ))
8881, 87mpbird 245 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ)
89 restsspw 15864 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆
90 dvnprodlem3.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
9189, 90sseldi 3565 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ 𝒫 𝑆)
92 elpwi 4116 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝒫 𝑆𝑋𝑆)
9391, 92syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝑆)
9486, 93eqsstrd 3601 . . . . . . . . . . . 12 (𝜑 → dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)
9588, 94jca 552 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆))
96 cnex 9874 . . . . . . . . . . . . 13 ℂ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
98 elpm2g 7738 . . . . . . . . . . . 12 ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9997, 76, 98syl2anc 690 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
10095, 99mpbird 245 . . . . . . . . . 10 (𝜑 → (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆))
101 dvn0 23438 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
10278, 100, 101syl2anc 690 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
103102adantr 479 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
104 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105104adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
106 dvnprodlem3.d . . . . . . . . . . . . . . . . . 18 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
107106a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
108 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 ∅))
109 elmapfn 7744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 Fn ∅)
110 fn0 5910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 Fn ∅ ↔ 𝑥 = ∅)
111109, 110sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 = ∅)
112 velsn 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
113111, 112sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) → 𝑥 ∈ {∅})
114112biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ {∅} → 𝑥 = ∅)
115 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = ∅ → 𝑥 = ∅)
116 f0 5984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅:∅⟶(0...𝑛)
117 ovex 6555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0...𝑛) ∈ V
118 0ex 4713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ ∈ V
119117, 118elmap 7750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ ((0...𝑛) ↑𝑚 ∅) ↔ ∅:∅⟶(0...𝑛))
120116, 119mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅ ∈ ((0...𝑛) ↑𝑚 ∅)
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑𝑚 ∅))
122115, 121eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
123114, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑𝑚 ∅))
124113, 123impbii 197 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
125124ax-gen 1712 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅})
126 dfcleq 2603 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑𝑚 ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑𝑚 ∅) ↔ 𝑥 ∈ {∅}))
127125, 126mpbir 219 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝑛) ↑𝑚 ∅) = {∅}
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 ∅) = {∅})
129108, 128eqtrd 2643 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑𝑚 𝑠) = {∅})
130 rabeq 3165 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑛) ↑𝑚 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
131129, 130syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
132 sumeq1 14216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = ∅ → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ ∅ (𝑐𝑡))
133132eqeq1d 2611 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛))
134133rabbidv 3163 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
135131, 134eqtrd 2643 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
136135mpteq2dv 4667 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
137136adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 = ∅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
138 0elpw 4755 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑇
139138a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ ∈ 𝒫 𝑇)
140 nn0ex 11148 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
141140mptex 6368 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V
142141a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V)
143107, 137, 139, 142fvmptd 6182 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
144 eqeq2 2620 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0))
145144rabbidv 3163 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
146145adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
147 0nn0 11157 . . . . . . . . . . . . . . . . 17 0 ∈ ℕ0
148147a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℕ0)
149 p0ex 4774 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
150149rabex 4735 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V
151150a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V)
152143, 146, 148, 151fvmptd 6182 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
153152adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
154 snidg 4152 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ V → ∅ ∈ {∅})
155118, 154ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ {∅}
156 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 0 = 0
157155, 156pm3.2i 469 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {∅} ∧ 0 = 0)
158 sum0 14248 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑡 ∈ ∅ (𝑐𝑡) = 0
159158a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
160159eqeq1d 2611 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 0 ↔ 0 = 0))
161160elrab 3330 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
162157, 161mpbir 219 . . . . . . . . . . . . . . . . . 18 ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
163162n0ii 3880 . . . . . . . . . . . . . . . . 17 ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅
164 eqid 2609 . . . . . . . . . . . . . . . . . 18 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
165 rabrsn 4202 . . . . . . . . . . . . . . . . . 18 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
167163, 166mtpor 1685 . . . . . . . . . . . . . . . 16 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}
168167a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
169 iftrue 4041 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
170169adantl 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
171168, 170eqtr4d 2646 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
172105, 153, 1713eqtrd 2647 . . . . . . . . . . . . 13 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
173172, 170eqtrd 2643 . . . . . . . . . . . 12 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
174173sumeq1d 14228 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
175 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘𝑘) = (!‘0))
176 fac0 12883 . . . . . . . . . . . . . . . . . . 19 (!‘0) = 1
177176a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘0) = 1)
178175, 177eqtrd 2643 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (!‘𝑘) = 1)
179178oveq1d 6542 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
180 prod0 14461 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ ∅ (!‘(𝑐𝑡)) = 1
181180oveq2i 6538 . . . . . . . . . . . . . . . . 17 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / 1)
182 1div1e1 10569 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
183181, 182eqtri 2631 . . . . . . . . . . . . . . . 16 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1
184179, 183syl6eq 2659 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1)
185 prod0 14461 . . . . . . . . . . . . . . . 16 𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1
186185a1i 11 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1)
187184, 186oveq12d 6545 . . . . . . . . . . . . . 14 (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
188187ad2antlr 758 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
189 1t1e1 11025 . . . . . . . . . . . . . 14 (1 · 1) = 1
190189a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
191188, 190eqtrd 2643 . . . . . . . . . . . 12 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
192191sumeq2dv 14230 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
193 ax-1cn 9851 . . . . . . . . . . . . 13 1 ∈ ℂ
194 eqidd 2610 . . . . . . . . . . . . . 14 (𝑐 = ∅ → 1 = 1)
195194sumsn 14268 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
196118, 193, 195mp2an 703 . . . . . . . . . . . 12 Σ𝑐 ∈ {∅}1 = 1
197196a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
198174, 192, 1973eqtrd 2647 . . . . . . . . . 10 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
199198mpteq2dv 4667 . . . . . . . . 9 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ 1))
200199eqcomd 2615 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
20175, 103, 2003eqtrd 2647 . . . . . . 7 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
202201a1d 25 . . . . . 6 ((𝜑𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
20371fveq1i 6089 . . . . . . . . 9 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘)
204203a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘))
20576adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
206205adantr 479 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
20790adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
208207adantr 479 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
209193a1i 11 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
210 elfznn0 12260 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
211210adantl 480 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
212 neqne 2789 . . . . . . . . . . . . 13 𝑘 = 0 → 𝑘 ≠ 0)
213212adantr 479 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
214211, 213jca 552 . . . . . . . . . . 11 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ0𝑘 ≠ 0))
215 elnnne0 11156 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
216214, 215sylibr 222 . . . . . . . . . 10 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
217216adantll 745 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
218206, 208, 209, 217dvnmptconst 38655 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘) = (𝑥𝑋 ↦ 0))
219143ad2antrr 757 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
220 eqeq2 2620 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘))
221220rabbidv 3163 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
222221adantl 480 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
223 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 𝑘)
224 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
225224eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = Σ𝑡 ∈ ∅ (𝑐𝑡))
226158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
227223, 225, 2263eqtrd 2647 . . . . . . . . . . . . . . . . . . . . 21 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 0)
228227adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
229228adantll 745 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
230 simpll 785 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → ¬ 𝑘 = 0)
231229, 230pm2.65da 597 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
232231ralrimiva 2948 . . . . . . . . . . . . . . . . 17 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
233 rabeq0 3910 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
234232, 233sylibr 222 . . . . . . . . . . . . . . . 16 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
235234adantr 479 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
236222, 235eqtrd 2643 . . . . . . . . . . . . . 14 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
237236adantll 745 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
238237adantlr 746 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
239210adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
240118a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
241219, 238, 239, 240fvmptd 6182 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
242241sumeq1d 14228 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
243 sum0 14248 . . . . . . . . . . 11 Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0
244243a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0)
245242, 244eqtr2d 2644 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
246245mpteq2dv 4667 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
247204, 218, 2463eqtrd 2647 . . . . . . 7 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
248247ex 448 . . . . . 6 ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
249202, 248pm2.61dan 827 . . . . 5 (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
250249ralrimiv 2947 . . . 4 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
251 simpll 785 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))))
252 fveq2 6088 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑡)‘𝑦))
253252prodeq2ad 38483 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑦))
254 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (𝐻𝑡) = (𝐻𝑢))
255254fveq1d 6090 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑢)‘𝑦))
256255cbvprodv 14434 . . . . . . . . . . . . . . . . 17 𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)
257256a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
258253, 257eqtrd 2643 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
259258cbvmptv 4672 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)) = (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
260259oveq2i 6538 . . . . . . . . . . . . 13 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))
261260fveq1i 6089 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘)
262 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → (𝑐𝑡) = (𝑐𝑢))
263262fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑢)))
264263cbvprodv 14434 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (!‘(𝑐𝑡)) = ∏𝑢𝑟 (!‘(𝑐𝑢))
265264oveq2i 6538 . . . . . . . . . . . . . . . . 17 ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢)))
266265a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))))
267 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
268267prodeq2ad 38483 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
269254oveq2d 6543 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑢 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑢)))
270269, 262fveq12d 6094 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)))
271270fveq1d 6090 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
272271cbvprodv 14434 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)
273272a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
274268, 273eqtrd 2643 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
275266, 274oveq12d 6545 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
276275sumeq2ad 38456 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
277 fveq1 6087 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → (𝑐𝑢) = (𝑑𝑢))
278277fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (!‘(𝑐𝑢)) = (!‘(𝑑𝑢)))
279278prodeq2ad 38483 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → ∏𝑢𝑟 (!‘(𝑐𝑢)) = ∏𝑢𝑟 (!‘(𝑑𝑢)))
280279oveq2d 6543 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))))
281277fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢)))
282281fveq1d 6090 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
283282prodeq2ad 38483 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
284280, 283oveq12d 6545 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
285284cbvsumv 14223 . . . . . . . . . . . . . . 15 Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
286285a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
287276, 286eqtrd 2643 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
288287cbvmptv 4672 . . . . . . . . . . . 12 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
289261, 288eqeq12i 2623 . . . . . . . . . . 11 (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
290289ralbii 2962 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
291290biimpi 204 . . . . . . . . 9 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
292291ad2antlr 758 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
293 simpr 475 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
29476ad3antrrr 761 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
29590ad3antrrr 761 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
296 dvnprodlem3.t . . . . . . . . . 10 (𝜑𝑇 ∈ Fin)
297296ad3antrrr 761 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
298 simp-4l 801 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝜑)
299 simpr 475 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝑡𝑇)
300 dvnprodlem3.h . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
301298, 299, 300syl2anc 690 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
302 dvnprodlem3.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
303302ad3antrrr 761 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
304 simplll 793 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
3053043ad2ant1 1074 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝜑)
306 simp2 1054 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝑡𝑇)
307 simp3 1055 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ∈ (0...𝑁))
308 eleq1 2675 . . . . . . . . . . . . 13 (𝑗 = → (𝑗 ∈ (0...𝑁) ↔ ∈ (0...𝑁)))
3093083anbi3d 1396 . . . . . . . . . . . 12 (𝑗 = → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∈ (0...𝑁))))
310 fveq2 6088 . . . . . . . . . . . . 13 (𝑗 = → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘))
311310feq1d 5929 . . . . . . . . . . . 12 (𝑗 = → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ))
312309, 311imbi12d 332 . . . . . . . . . . 11 (𝑗 = → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)))
313 dvnprodlem3.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
314312, 313chvarv 2250 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
315305, 306, 307, 314syl3anc 1317 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
316 simprl 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑟𝑇)
317316ad2antrr 757 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟𝑇)
318 simprr 791 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑧 ∈ (𝑇𝑟))
319318ad2antrr 757 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇𝑟))
320260eqcomi 2618 . . . . . . . . . . . . . . 15 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
321320a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
322 id 22 . . . . . . . . . . . . . 14 (𝑘 = 𝑙𝑘 = 𝑙)
323321, 322fveq12d 6094 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙))
324288eqcomi 2618 . . . . . . . . . . . . . . 15 (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
325324a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
326 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
327326oveq1d 6542 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
328327oveq1d 6542 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
329328sumeq2ad 38456 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
330 fveq2 6088 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝐷𝑟)‘𝑘) = ((𝐷𝑟)‘𝑙))
331330sumeq1d 14228 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
332329, 331eqtrd 2643 . . . . . . . . . . . . . . 15 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
333332mpteq2dv 4667 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
334325, 333eqtrd 2643 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
335323, 334eqeq12d 2624 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
336335cbvralv 3146 . . . . . . . . . . 11 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
337336biimpi 204 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
338337ad2antlr 758 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
339 simpr 475 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
340 fveq1 6087 . . . . . . . . . . . 12 (𝑑 = 𝑐 → (𝑑𝑧) = (𝑐𝑧))
341340oveq2d 6543 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑗 − (𝑑𝑧)) = (𝑗 − (𝑐𝑧)))
342 reseq1 5298 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑑𝑟) = (𝑐𝑟))
343341, 342opeq12d 4342 . . . . . . . . . 10 (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩ = ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
344343cbvmptv 4672 . . . . . . . . 9 (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
345294, 295, 297, 301, 303, 315, 106, 317, 319, 338, 339, 344dvnprodlem2 38661 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
346251, 292, 293, 345syl21anc 1316 . . . . . . 7 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
347346ralrimiva 2948 . . . . . 6 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
348 fveq2 6088 . . . . . . . 8 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
349 fveq2 6088 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
350349oveq1d 6542 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
351350oveq1d 6542 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
352351sumeq2ad 38456 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
353 fveq2 6088 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
354353sumeq1d 14228 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
355352, 354eqtrd 2643 . . . . . . . . 9 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
356355mpteq2dv 4667 . . . . . . . 8 (𝑗 = 𝑘 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
357348, 356eqeq12d 2624 . . . . . . 7 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
358357cbvralv 3146 . . . . . 6 (∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
359347, 358sylib 206 . . . . 5 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
360359ex 448 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
36116, 32, 48, 68, 250, 360, 296findcard2d 8065 . . 3 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
362 nn0uz 11557 . . . . 5 0 = (ℤ‘0)
363302, 362syl6eleq 2697 . . . 4 (𝜑𝑁 ∈ (ℤ‘0))
364 eluzfz2 12178 . . . 4 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
365363, 364syl 17 . . 3 (𝜑𝑁 ∈ (0...𝑁))
366 fveq2 6088 . . . . 5 (𝑘 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑁))
367 fveq2 6088 . . . . . . . 8 (𝑘 = 𝑁 → ((𝐷𝑇)‘𝑘) = ((𝐷𝑇)‘𝑁))
368367sumeq1d 14228 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
369 fveq2 6088 . . . . . . . . . 10 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
370369oveq1d 6542 . . . . . . . . 9 (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) = ((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
371370oveq1d 6542 . . . . . . . 8 (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
372371sumeq2ad 38456 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
373368, 372eqtrd 2643 . . . . . 6 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
374373mpteq2dv 4667 . . . . 5 (𝑘 = 𝑁 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
375366, 374eqeq12d 2624 . . . 4 (𝑘 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
376375rspccva 3280 . . 3 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
377361, 365, 376syl2anc 690 . 2 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
378 oveq2 6535 . . . . . . . . . . 11 (𝑠 = 𝑇 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇))
379 rabeq 3165 . . . . . . . . . . 11 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑇) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
380378, 379syl 17 . . . . . . . . . 10 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
381 sumeq1 14216 . . . . . . . . . . . 12 (𝑠 = 𝑇 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑇 (𝑐𝑡))
382381eqeq1d 2611 . . . . . . . . . . 11 (𝑠 = 𝑇 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑇 (𝑐𝑡) = 𝑛))
383382rabbidv 3163 . . . . . . . . . 10 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
384380, 383eqtrd 2643 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
385384mpteq2dv 4667 . . . . . . . 8 (𝑠 = 𝑇 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
386385adantl 480 . . . . . . 7 ((𝜑𝑠 = 𝑇) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
387 pwidg 4120 . . . . . . . 8 (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
388296, 387syl 17 . . . . . . 7 (𝜑𝑇 ∈ 𝒫 𝑇)
389140mptex 6368 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V
390389a1i 11 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V)
391107, 386, 388, 390fvmptd 6182 . . . . . 6 (𝜑 → (𝐷𝑇) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
392 dvnprodlem3.c . . . . . . 7 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
393392a1i 11 . . . . . 6 (𝜑𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
394391, 393eqtr4d 2646 . . . . 5 (𝜑 → (𝐷𝑇) = 𝐶)
395394fveq1d 6090 . . . 4 (𝜑 → ((𝐷𝑇)‘𝑁) = (𝐶𝑁))
396395sumeq1d 14228 . . 3 (𝜑 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
397396mpteq2dv 4667 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
398377, 397eqtrd 2643 1 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030  wal 1472   = wceq 1474  wcel 1976  wne 2779  wral 2895  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  wss 3539  c0 3873  ifcif 4035  𝒫 cpw 4107  {csn 4124  {cpr 4126  cop 4130  cmpt 4637  dom cdm 5028  cres 5030   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  𝑚 cmap 7722  pm cpm 7723  Fincfn 7819  cc 9791  cr 9792  0cc0 9793  1c1 9794   · cmul 9798  cmin 10118   / cdiv 10536  cn 10870  0cn0 11142  cuz 11522  ...cfz 12155  !cfa 12880  Σcsu 14213  cprod 14423  t crest 15853  TopOpenctopn 15854  fldccnfld 19516   D𝑛 cdvn 23379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-prod 14424  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-limc 23381  df-dv 23382  df-dvn 23383
This theorem is referenced by:  dvnprod  38663
  Copyright terms: Public domain W3C validator