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

Proof of Theorem dvnprodlem3
Dummy variables 𝑑 𝑘 𝑙 𝑟 𝑧 𝑦 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodeq1 15691 . . . . . . . . 9 (𝑠 = ∅ → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))
21mpteq2dv 5189 . . . . . . . 8 (𝑠 = ∅ → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))
32oveq2d 7331 . . . . . . 7 (𝑠 = ∅ → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))))
43fveq1d 6813 . . . . . 6 (𝑠 = ∅ → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘))
5 fveq2 6811 . . . . . . . . . 10 (𝑠 = ∅ → (𝐷𝑠) = (𝐷‘∅))
65fveq1d 6813 . . . . . . . . 9 (𝑠 = ∅ → ((𝐷𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
76sumeq1d 15485 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
8 prodeq1 15691 . . . . . . . . . . 11 (𝑠 = ∅ → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐𝑡)))
98oveq2d 7331 . . . . . . . . . 10 (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
10 prodeq1 15691 . . . . . . . . . 10 (𝑠 = ∅ → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
119, 10oveq12d 7333 . . . . . . . . 9 (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1211sumeq2sdv 15488 . . . . . . . 8 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
137, 12eqtrd 2777 . . . . . . 7 (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
1413mpteq2dv 5189 . . . . . 6 (𝑠 = ∅ → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
154, 14eqeq12d 2753 . . . . 5 (𝑠 = ∅ → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
1615ralbidv 3171 . . . 4 (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
17 prodeq1 15691 . . . . . . . . 9 (𝑠 = 𝑟 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))
1817mpteq2dv 5189 . . . . . . . 8 (𝑠 = 𝑟 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
1918oveq2d 7331 . . . . . . 7 (𝑠 = 𝑟 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
2019fveq1d 6813 . . . . . 6 (𝑠 = 𝑟 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘))
21 fveq2 6811 . . . . . . . . . 10 (𝑠 = 𝑟 → (𝐷𝑠) = (𝐷𝑟))
2221fveq1d 6813 . . . . . . . . 9 (𝑠 = 𝑟 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑟)‘𝑘))
2322sumeq1d 15485 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
24 prodeq1 15691 . . . . . . . . . . 11 (𝑠 = 𝑟 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑟 (!‘(𝑐𝑡)))
2524oveq2d 7331 . . . . . . . . . 10 (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
26 prodeq1 15691 . . . . . . . . . 10 (𝑠 = 𝑟 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
2725, 26oveq12d 7333 . . . . . . . . 9 (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2827sumeq2sdv 15488 . . . . . . . 8 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
2923, 28eqtrd 2777 . . . . . . 7 (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
3029mpteq2dv 5189 . . . . . 6 (𝑠 = 𝑟 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
3120, 30eqeq12d 2753 . . . . 5 (𝑠 = 𝑟 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
3231ralbidv 3171 . . . 4 (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
33 prodeq1 15691 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))
3433mpteq2dv 5189 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))
3534oveq2d 7331 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥))))
3635fveq1d 6813 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
37 fveq2 6811 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
3837fveq1d 6813 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
3938sumeq1d 15485 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
40 prodeq1 15691 . . . . . . . . . . 11 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡)))
4140oveq2d 7331 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
42 prodeq1 15691 . . . . . . . . . 10 (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
4341, 42oveq12d 7333 . . . . . . . . 9 (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4443sumeq2sdv 15488 . . . . . . . 8 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4539, 44eqtrd 2777 . . . . . . 7 (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
4645mpteq2dv 5189 . . . . . 6 (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
4736, 46eqeq12d 2753 . . . . 5 (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
4847ralbidv 3171 . . . 4 (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
49 prodeq1 15691 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5049mpteq2dv 5189 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
51 dvnprodlem3.f . . . . . . . . . . 11 𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥))
5251a1i 11 . . . . . . . . . 10 (𝑠 = 𝑇𝐹 = (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)))
5352eqcomd 2743 . . . . . . . . 9 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑇 ((𝐻𝑡)‘𝑥)) = 𝐹)
5450, 53eqtrd 2777 . . . . . . . 8 (𝑠 = 𝑇 → (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)) = 𝐹)
5554oveq2d 7331 . . . . . . 7 (𝑠 = 𝑇 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 𝐹))
5655fveq1d 6813 . . . . . 6 (𝑠 = 𝑇 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘))
57 fveq2 6811 . . . . . . . . . 10 (𝑠 = 𝑇 → (𝐷𝑠) = (𝐷𝑇))
5857fveq1d 6813 . . . . . . . . 9 (𝑠 = 𝑇 → ((𝐷𝑠)‘𝑘) = ((𝐷𝑇)‘𝑘))
5958sumeq1d 15485 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
60 prodeq1 15691 . . . . . . . . . . 11 (𝑠 = 𝑇 → ∏𝑡𝑠 (!‘(𝑐𝑡)) = ∏𝑡𝑇 (!‘(𝑐𝑡)))
6160oveq2d 7331 . . . . . . . . . 10 (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
62 prodeq1 15691 . . . . . . . . . 10 (𝑠 = 𝑇 → ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
6361, 62oveq12d 7333 . . . . . . . . 9 (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6463sumeq2sdv 15488 . . . . . . . 8 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6559, 64eqtrd 2777 . . . . . . 7 (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
6665mpteq2dv 5189 . . . . . 6 (𝑠 = 𝑇 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
6756, 66eqeq12d 2753 . . . . 5 (𝑠 = 𝑇 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
6867ralbidv 3171 . . . 4 (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑠 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡𝑠 (!‘(𝑐𝑡))) · ∏𝑡𝑠 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
69 prod0 15725 . . . . . . . . . . . . 13 𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥) = 1
7069mpteq2i 5192 . . . . . . . . . . . 12 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ 1)
7170oveq2i 7326 . . . . . . . . . . 11 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1))
7271a1i 11 . . . . . . . . . 10 (𝑘 = 0 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ 1)))
73 id 22 . . . . . . . . . 10 (𝑘 = 0 → 𝑘 = 0)
7472, 73fveq12d 6818 . . . . . . . . 9 (𝑘 = 0 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
7574adantl 482 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0))
76 dvnprodlem3.s . . . . . . . . . . 11 (𝜑𝑆 ∈ {ℝ, ℂ})
77 recnprss 25140 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
7876, 77syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
79 1cnd 11043 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 1 ∈ ℂ)
8079fmpttd 7028 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ 1):𝑋⟶ℂ)
81 1re 11048 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
8281rgenw 3066 . . . . . . . . . . . . . . . 16 𝑥𝑋 1 ∈ ℝ
83 dmmptg 6167 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 1 ∈ ℝ → dom (𝑥𝑋 ↦ 1) = 𝑋)
8482, 83ax-mp 5 . . . . . . . . . . . . . . 15 dom (𝑥𝑋 ↦ 1) = 𝑋
8584a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑥𝑋 ↦ 1) = 𝑋)
8685feq2d 6623 . . . . . . . . . . . . 13 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ↔ (𝑥𝑋 ↦ 1):𝑋⟶ℂ))
8780, 86mpbird 256 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ)
88 restsspw 17212 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆
89 dvnprodlem3.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
9088, 89sselid 3929 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ 𝒫 𝑆)
91 elpwi 4552 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝒫 𝑆𝑋𝑆)
9290, 91syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝑆)
9385, 92eqsstrd 3969 . . . . . . . . . . . 12 (𝜑 → dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)
9487, 93jca 512 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆))
95 cnex 11025 . . . . . . . . . . . . 13 ℂ ∈ V
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ∈ V)
97 elpm2g 8680 . . . . . . . . . . . 12 ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9896, 76, 97syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆) ↔ ((𝑥𝑋 ↦ 1):dom (𝑥𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥𝑋 ↦ 1) ⊆ 𝑆)))
9994, 98mpbird 256 . . . . . . . . . 10 (𝜑 → (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆))
100 dvn0 25160 . . . . . . . . . 10 ((𝑆 ⊆ ℂ ∧ (𝑥𝑋 ↦ 1) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
10178, 99, 100syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
102101adantr 481 . . . . . . . 8 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘0) = (𝑥𝑋 ↦ 1))
103 fveq2 6811 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
104103adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105 dvnprodlem3.d . . . . . . . . . . . . . . . . 17 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
106 oveq2 7323 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m ∅))
107 elmapfn 8701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 Fn ∅)
108 fn0 6601 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 Fn ∅ ↔ 𝑥 = ∅)
109107, 108sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 = ∅)
110 velsn 4587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
111109, 110sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ((0...𝑛) ↑m ∅) → 𝑥 ∈ {∅})
112110biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ {∅} → 𝑥 = ∅)
113 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → 𝑥 = ∅)
114 f0 6692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅:∅⟶(0...𝑛)
115 ovex 7348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0...𝑛) ∈ V
116 0ex 5246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ V
117115, 116elmap 8707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∅ ∈ ((0...𝑛) ↑m ∅) ↔ ∅:∅⟶(0...𝑛))
118114, 117mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ∅ ∈ ((0...𝑛) ↑m ∅)
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑m ∅))
120113, 119eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑m ∅))
121112, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑m ∅))
122111, 121impbii 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅})
123122ax-gen 1796 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅})
124 dfcleq 2730 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑛) ↑m ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑m ∅) ↔ 𝑥 ∈ {∅}))
125123, 124mpbir 230 . . . . . . . . . . . . . . . . . . . . . 22 ((0...𝑛) ↑m ∅) = {∅}
126125a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → ((0...𝑛) ↑m ∅) = {∅})
127106, 126eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → ((0...𝑛) ↑m 𝑠) = {∅})
128 rabeq 3417 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑m 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
129127, 128syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
130 sumeq1 15472 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ∅ → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ ∅ (𝑐𝑡))
131130eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ∅ → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛))
132131rabbidv 3412 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
133129, 132eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛})
134133mpteq2dv 5189 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
135 0elpw 5293 . . . . . . . . . . . . . . . . . 18 ∅ ∈ 𝒫 𝑇
136135a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ ∈ 𝒫 𝑇)
137 nn0ex 12312 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
138137mptex 7138 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V
139138a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}) ∈ V)
140105, 134, 136, 139fvmptd3 6937 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
141 eqeq2 2749 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0))
142141rabbidv 3412 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
143142adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
144 0nn0 12321 . . . . . . . . . . . . . . . . 17 0 ∈ ℕ0
145144a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℕ0)
146 p0ex 5322 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
147146rabex 5271 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V
148147a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ∈ V)
149140, 143, 145, 148fvmptd 6921 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
150149adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0})
151 snidg 4605 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ V → ∅ ∈ {∅})
152116, 151ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ {∅}
153 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 0 = 0
154152, 153pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {∅} ∧ 0 = 0)
155 sum0 15505 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑡 ∈ ∅ (𝑐𝑡) = 0
156155a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
157156eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 0 ↔ 0 = 0))
158157elrab 3634 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
159154, 158mpbir 230 . . . . . . . . . . . . . . . . . 18 ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
160159n0ii 4281 . . . . . . . . . . . . . . . . 17 ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅
161 eqid 2737 . . . . . . . . . . . . . . . . . 18 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0}
162 rabrsn 4670 . . . . . . . . . . . . . . . . . 18 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
164160, 163mtpor 1771 . . . . . . . . . . . . . . . 16 {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅}
165164a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = {∅})
166 iftrue 4477 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
167166adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
168165, 167eqtr4d 2780 . . . . . . . . . . . . . 14 ((𝜑𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
169104, 150, 1683eqtrd 2781 . . . . . . . . . . . . 13 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
170169, 167eqtrd 2777 . . . . . . . . . . . 12 ((𝜑𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
171170sumeq1d 15485 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
172 fveq2 6811 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘𝑘) = (!‘0))
173 fac0 14063 . . . . . . . . . . . . . . . . . . 19 (!‘0) = 1
174173a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (!‘0) = 1)
175172, 174eqtrd 2777 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (!‘𝑘) = 1)
176175oveq1d 7330 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))))
177 prod0 15725 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ ∅ (!‘(𝑐𝑡)) = 1
178177oveq2i 7326 . . . . . . . . . . . . . . . . 17 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = (1 / 1)
179 1div1e1 11738 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
180178, 179eqtri 2765 . . . . . . . . . . . . . . . 16 (1 / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1
181176, 180eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) = 1)
182 prod0 15725 . . . . . . . . . . . . . . . 16 𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1
183182a1i 11 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = 1)
184181, 183oveq12d 7333 . . . . . . . . . . . . . 14 (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
185184ad2antlr 724 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (1 · 1))
186 1t1e1 12208 . . . . . . . . . . . . . 14 (1 · 1) = 1
187186a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
188185, 187eqtrd 2777 . . . . . . . . . . . 12 (((𝜑𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
189188sumeq2dv 15487 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
190 ax-1cn 11002 . . . . . . . . . . . . 13 1 ∈ ℂ
191 eqidd 2738 . . . . . . . . . . . . . 14 (𝑐 = ∅ → 1 = 1)
192191sumsn 15530 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
193116, 190, 192mp2an 689 . . . . . . . . . . . 12 Σ𝑐 ∈ {∅}1 = 1
194193a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
195171, 189, 1943eqtrd 2781 . . . . . . . . . 10 ((𝜑𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 1)
196195mpteq2dv 5189 . . . . . . . . 9 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ 1))
197196eqcomd 2743 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑥𝑋 ↦ 1) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
19875, 102, 1973eqtrd 2781 . . . . . . 7 ((𝜑𝑘 = 0) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
199198a1d 25 . . . . . 6 ((𝜑𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
20071fveq1i 6812 . . . . . . . . 9 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘)
201200a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘))
20276adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
203202adantr 481 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
20489adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
205204adantr 481 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
206190a1i 11 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
207 elfznn0 13422 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
208207adantl 482 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
209 neqne 2949 . . . . . . . . . . . . 13 𝑘 = 0 → 𝑘 ≠ 0)
210209adantr 481 . . . . . . . . . . . 12 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
211208, 210jca 512 . . . . . . . . . . 11 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ0𝑘 ≠ 0))
212 elnnne0 12320 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
213211, 212sylibr 233 . . . . . . . . . 10 ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
214213adantll 711 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
215203, 205, 206, 214dvnmptconst 43719 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ 1))‘𝑘) = (𝑥𝑋 ↦ 0))
216140ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛}))
217 eqeq2 2749 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘))
218217rabbidv 3412 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
219218adantl 482 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘})
220 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 𝑘)
221 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
222221eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = Σ𝑡 ∈ ∅ (𝑐𝑡))
223155a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐𝑡) = 0)
224220, 222, 2233eqtrd 2781 . . . . . . . . . . . . . . . . . . . . 21 𝑡 ∈ ∅ (𝑐𝑡) = 𝑘𝑘 = 0)
225224adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
226225adantll 711 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → 𝑘 = 0)
227 simpll 764 . . . . . . . . . . . . . . . . . . 19 (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘) → ¬ 𝑘 = 0)
228226, 227pm2.65da 814 . . . . . . . . . . . . . . . . . 18 ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
229228ralrimiva 3140 . . . . . . . . . . . . . . . . 17 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
230 rabeq0 4329 . . . . . . . . . . . . . . . . 17 ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘)
231229, 230sylibr 233 . . . . . . . . . . . . . . . 16 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
232231adantr 481 . . . . . . . . . . . . . . 15 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑘} = ∅)
233219, 232eqtrd 2777 . . . . . . . . . . . . . 14 ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
234233adantll 711 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
235234adantlr 712 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐𝑡) = 𝑛} = ∅)
236207adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
237116a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
238216, 235, 236, 237fvmptd 6921 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
239238sumeq1d 15485 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
240 sum0 15505 . . . . . . . . . . 11 Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0
241240a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = 0)
242239, 241eqtr2d 2778 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
243242mpteq2dv 5189 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥𝑋 ↦ 0) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
244201, 215, 2433eqtrd 2781 . . . . . . 7 (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
245244ex 413 . . . . . 6 ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
246199, 245pm2.61dan 810 . . . . 5 (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
247246ralrimiv 3139 . . . 4 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
248 simpll 764 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))))
249 fveq2 6811 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑡)‘𝑦))
250249prodeq2ad 43370 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑡𝑟 ((𝐻𝑡)‘𝑦))
251 fveq2 6811 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (𝐻𝑡) = (𝐻𝑢))
252251fveq1d 6813 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑢 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑢)‘𝑦))
253252cbvprodv 15698 . . . . . . . . . . . . . . . . 17 𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)
254253a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑦) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
255250, 254eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ∏𝑡𝑟 ((𝐻𝑡)‘𝑥) = ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
256255cbvmptv 5200 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)) = (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))
257256oveq2i 7326 . . . . . . . . . . . . 13 (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))
258257fveq1i 6812 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘)
259 fveq2 6811 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → (𝑐𝑡) = (𝑐𝑢))
260259fveq2d 6815 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑢)))
261260cbvprodv 15698 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (!‘(𝑐𝑡)) = ∏𝑢𝑟 (!‘(𝑐𝑢))
262261oveq2i 7326 . . . . . . . . . . . . . . . . 17 ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢)))
263262a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))))
264 fveq2 6811 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
265264prodeq2ad 43370 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦))
266251oveq2d 7331 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑢 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑢)))
267266, 259fveq12d 6818 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)))
268267fveq1d 6813 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑢 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
269268cbvprodv 15698 . . . . . . . . . . . . . . . . . 18 𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)
270269a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
271265, 270eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦))
272263, 271oveq12d 7333 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
273272sumeq2sdv 15488 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)))
274 fveq1 6810 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑑 → (𝑐𝑢) = (𝑑𝑢))
275274fveq2d 6815 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → (!‘(𝑐𝑢)) = (!‘(𝑑𝑢)))
276275prodeq2ad 43370 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → ∏𝑢𝑟 (!‘(𝑐𝑢)) = ∏𝑢𝑟 (!‘(𝑑𝑢)))
277276oveq2d 7331 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) = ((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))))
278274fveq2d 6815 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑑 → ((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢)) = ((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢)))
279278fveq1d 6813 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑑 → (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
280279prodeq2ad 43370 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑑 → ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦) = ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
281277, 280oveq12d 7333 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
282281cbvsumv 15480 . . . . . . . . . . . . . . 15 Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))
283282a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑐𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑐𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
284273, 283eqtrd 2777 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
285284cbvmptv 5200 . . . . . . . . . . . 12 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))
286258, 285eqeq12i 2755 . . . . . . . . . . 11 (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
287286ralbii 3093 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
288287biimpi 215 . . . . . . . . 9 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
289288ad2antlr 724 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))))
290 simpr 485 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
29176ad3antrrr 727 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
29289ad3antrrr 727 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
293 dvnprodlem3.t . . . . . . . . . 10 (𝜑𝑇 ∈ Fin)
294293ad3antrrr 727 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
295 simp-4l 780 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝜑)
296 simpr 485 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → 𝑡𝑇)
297 dvnprodlem3.h . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
298295, 296, 297syl2anc 584 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
299 dvnprodlem3.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
300299ad3antrrr 727 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
301 simplll 772 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
3023013ad2ant1 1132 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝜑)
303 simp2 1136 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → 𝑡𝑇)
304 simp3 1137 . . . . . . . . . 10 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ∈ (0...𝑁))
305 eleq1w 2820 . . . . . . . . . . . . 13 (𝑗 = → (𝑗 ∈ (0...𝑁) ↔ ∈ (0...𝑁)))
3063053anbi3d 1441 . . . . . . . . . . . 12 (𝑗 = → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∈ (0...𝑁))))
307 fveq2 6811 . . . . . . . . . . . . 13 (𝑗 = → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘))
308307feq1d 6622 . . . . . . . . . . . 12 (𝑗 = → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ))
309306, 308imbi12d 344 . . . . . . . . . . 11 (𝑗 = → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)))
310 dvnprodlem3.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
311309, 310chvarvv 2001 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
312302, 303, 304, 311syl3anc 1370 . . . . . . . . 9 (((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡𝑇 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘):𝑋⟶ℂ)
313 simprl 768 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑟𝑇)
314313ad2antrr 723 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟𝑇)
315 simprr 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → 𝑧 ∈ (𝑇𝑟))
316315ad2antrr 723 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇𝑟))
317257eqcomi 2746 . . . . . . . . . . . . . . 15 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))
318317a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥))))
319 id 22 . . . . . . . . . . . . . 14 (𝑘 = 𝑙𝑘 = 𝑙)
320318, 319fveq12d 6818 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙))
321285eqcomi 2746 . . . . . . . . . . . . . . 15 (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
322321a1i 11 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
323 fveq2 6811 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
324323oveq1d 7330 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) = ((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))))
325324oveq1d 7330 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
326325sumeq2sdv 15488 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
327 fveq2 6811 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝐷𝑟)‘𝑘) = ((𝐷𝑟)‘𝑙))
328327sumeq1d 15485 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
329326, 328eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
330329mpteq2dv 5189 . . . . . . . . . . . . . 14 (𝑘 = 𝑙 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
331322, 330eqtrd 2777 . . . . . . . . . . . . 13 (𝑘 = 𝑙 → (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
332320, 331eqeq12d 2753 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
333332cbvralvw 3222 . . . . . . . . . . 11 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
334333biimpi 215 . . . . . . . . . 10 (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
335334ad2antlr 724 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑙) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
336 simpr 485 . . . . . . . . 9 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
337 fveq1 6810 . . . . . . . . . . . 12 (𝑑 = 𝑐 → (𝑑𝑧) = (𝑐𝑧))
338337oveq2d 7331 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑗 − (𝑑𝑧)) = (𝑗 − (𝑐𝑧)))
339 reseq1 5904 . . . . . . . . . . 11 (𝑑 = 𝑐 → (𝑑𝑟) = (𝑐𝑟))
340338, 339opeq12d 4823 . . . . . . . . . 10 (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩ = ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
341340cbvmptv 5200 . . . . . . . . 9 (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑𝑧)), (𝑑𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐𝑧)), (𝑐𝑟)⟩)
342291, 292, 294, 298, 300, 312, 105, 314, 316, 335, 336, 341dvnprodlem2 43725 . . . . . . . 8 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑢𝑟 ((𝐻𝑢)‘𝑦)))‘𝑘) = (𝑦𝑋 ↦ Σ𝑑 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢𝑟 (!‘(𝑑𝑢))) · ∏𝑢𝑟 (((𝑆 D𝑛 (𝐻𝑢))‘(𝑑𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
343248, 289, 290, 342syl21anc 835 . . . . . . 7 ((((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
344343ralrimiva 3140 . . . . . 6 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
345 fveq2 6811 . . . . . . . 8 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘))
346 fveq2 6811 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
347346oveq1d 7330 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))))
348347oveq1d 7330 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
349348sumeq2sdv 15488 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
350 fveq2 6811 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
351350sumeq1d 15485 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
352349, 351eqtrd 2777 . . . . . . . . 9 (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
353352mpteq2dv 5189 . . . . . . . 8 (𝑗 = 𝑘 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
354345, 353eqeq12d 2753 . . . . . . 7 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
355354cbvralvw 3222 . . . . . 6 (∀𝑗 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑗) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
356344, 355sylib 217 . . . . 5 (((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
357356ex 413 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑧 ∈ (𝑇𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑟 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡𝑟 (!‘(𝑐𝑡))) · ∏𝑡𝑟 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
35816, 32, 48, 68, 247, 357, 293findcard2d 9008 . . 3 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
359 nn0uz 12693 . . . . 5 0 = (ℤ‘0)
360299, 359eleqtrdi 2848 . . . 4 (𝜑𝑁 ∈ (ℤ‘0))
361 eluzfz2 13337 . . . 4 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
362360, 361syl 17 . . 3 (𝜑𝑁 ∈ (0...𝑁))
363 fveq2 6811 . . . . 5 (𝑘 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑁))
364 fveq2 6811 . . . . . . . 8 (𝑘 = 𝑁 → ((𝐷𝑇)‘𝑘) = ((𝐷𝑇)‘𝑁))
365364sumeq1d 15485 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
366 fveq2 6811 . . . . . . . . . 10 (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
367366oveq1d 7330 . . . . . . . . 9 (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) = ((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))))
368367oveq1d 7330 . . . . . . . 8 (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
369368sumeq2sdv 15488 . . . . . . 7 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
370365, 369eqtrd 2777 . . . . . 6 (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
371370mpteq2dv 5189 . . . . 5 (𝑘 = 𝑁 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
372363, 371eqeq12d 2753 . . . 4 (𝑘 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
373372rspccva 3569 . . 3 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 𝐹)‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
374358, 362, 373syl2anc 584 . 2 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
375 oveq2 7323 . . . . . . . . . 10 (𝑠 = 𝑇 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑇))
376 rabeq 3417 . . . . . . . . . 10 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑇) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
377375, 376syl 17 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
378 sumeq1 15472 . . . . . . . . . . 11 (𝑠 = 𝑇 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑇 (𝑐𝑡))
379378eqeq1d 2739 . . . . . . . . . 10 (𝑠 = 𝑇 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑇 (𝑐𝑡) = 𝑛))
380379rabbidv 3412 . . . . . . . . 9 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
381377, 380eqtrd 2777 . . . . . . . 8 (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
382381mpteq2dv 5189 . . . . . . 7 (𝑠 = 𝑇 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
383 pwidg 4565 . . . . . . . 8 (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
384293, 383syl 17 . . . . . . 7 (𝜑𝑇 ∈ 𝒫 𝑇)
385137mptex 7138 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V
386385a1i 11 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}) ∈ V)
387105, 382, 384, 386fvmptd3 6937 . . . . . 6 (𝜑 → (𝐷𝑇) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
388 dvnprodlem3.c . . . . . . 7 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛})
389388a1i 11 . . . . . 6 (𝜑𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡𝑇 (𝑐𝑡) = 𝑛}))
390387, 389eqtr4d 2780 . . . . 5 (𝜑 → (𝐷𝑇) = 𝐶)
391390fveq1d 6813 . . . 4 (𝜑 → ((𝐷𝑇)‘𝑁) = (𝐶𝑁))
392391sumeq1d 15485 . . 3 (𝜑 → Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
393392mpteq2dv 5189 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐷𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
394374, 393eqtrd 2777 1 (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥𝑋 ↦ Σ𝑐 ∈ (𝐶𝑁)(((!‘𝑁) / ∏𝑡𝑇 (!‘(𝑐𝑡))) · ∏𝑡𝑇 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086  wal 1538   = wceq 1540  wcel 2105  wne 2941  wral 3062  {crab 3404  Vcvv 3441  cdif 3894  cun 3895  wss 3897  c0 4267  ifcif 4471  𝒫 cpw 4545  {csn 4571  {cpr 4573  cop 4577  cmpt 5170  dom cdm 5607  cres 5609   Fn wfn 6460  wf 6461  cfv 6465  (class class class)co 7315  m cmap 8663  pm cpm 8664  Fincfn 8781  cc 10942  cr 10943  0cc0 10944  1c1 10945   · cmul 10949  cmin 11278   / cdiv 11705  cn 12046  0cn0 12306  cuz 12655  ...cfz 13312  !cfa 14060  Σcsu 15469  cprod 15687  t crest 17201  TopOpenctopn 17202  fldccnfld 20669   D𝑛 cdvn 25100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-inf2 9470  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022  ax-addf 11023  ax-mulf 11024
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-2o 8345  df-er 8546  df-map 8665  df-pm 8666  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-fi 9240  df-sup 9271  df-inf 9272  df-oi 9339  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-z 12393  df-dec 12511  df-uz 12656  df-q 12762  df-rp 12804  df-xneg 12921  df-xadd 12922  df-xmul 12923  df-ico 13158  df-icc 13159  df-fz 13313  df-fzo 13456  df-seq 13795  df-exp 13856  df-fac 14061  df-bc 14090  df-hash 14118  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019  df-clim 15269  df-sum 15470  df-prod 15688  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-rest 17203  df-topn 17204  df-0g 17222  df-gsum 17223  df-topgen 17224  df-pt 17225  df-prds 17228  df-xrs 17283  df-qtop 17288  df-imas 17289  df-xps 17291  df-mre 17365  df-mrc 17366  df-acs 17368  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-submnd 18501  df-mulg 18770  df-cntz 18992  df-cmn 19456  df-psmet 20661  df-xmet 20662  df-met 20663  df-bl 20664  df-mopn 20665  df-fbas 20666  df-fg 20667  df-cnfld 20670  df-top 22115  df-topon 22132  df-topsp 22154  df-bases 22168  df-cld 22242  df-ntr 22243  df-cls 22244  df-nei 22321  df-lp 22359  df-perf 22360  df-cn 22450  df-cnp 22451  df-haus 22538  df-tx 22785  df-hmeo 22978  df-fil 23069  df-fm 23161  df-flim 23162  df-flf 23163  df-xms 23545  df-ms 23546  df-tms 23547  df-cncf 24113  df-limc 25102  df-dv 25103  df-dvn 25104
This theorem is referenced by:  dvnprod  43727
  Copyright terms: Public domain W3C validator