dvnprodlem3 - Mathbox for Glauco Siliprandi

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

Theorem dvnprodlem3 38838

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	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
dvnprodlem3.dvnh	⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ)
dvnprodlem3.f	⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥))
dvnprodlem3.d	⊢ 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
dvnprodlem3.c	⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((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.

Step	Hyp	Ref	Expression
1		prodeq1 14478	. . . . . . . . 9 ⊢ (𝑠 = ∅ → ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥) = ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥))
2	1	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑠 = ∅ → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))
3	2	oveq2d 6565	. . . . . . 7 ⊢ (𝑠 = ∅ → (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥))))
4	3	fveq1d 6105	. . . . . 6 ⊢ (𝑠 = ∅ → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘))
5		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (𝐷‘𝑠) = (𝐷‘∅))
6	5	fveq1d 6105	. . . . . . . . 9 ⊢ (𝑠 = ∅ → ((𝐷‘𝑠)‘𝑘) = ((𝐷‘∅)‘𝑘))
7	6	sumeq1d 14279	. . . . . . . 8 ⊢ (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
8		prodeq1 14478	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡)) = ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡)))
9	8	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → ((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))))
10		prodeq1 14478	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))
11	9, 10	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
12	11	sumeq2ad 38632	. . . . . . . 8 ⊢ (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
13	7, 12	eqtrd 2644	. . . . . . 7 ⊢ (𝑠 = ∅ → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
14	13	mpteq2dv 4673	. . . . . 6 ⊢ (𝑠 = ∅ → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
15	4, 14	eqeq12d 2625	. . . . 5 ⊢ (𝑠 = ∅ → (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
16	15	ralbidv 2969	. . . 4 ⊢ (𝑠 = ∅ → (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
17		prodeq1 14478	. . . . . . . . 9 ⊢ (𝑠 = 𝑟 → ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥) = ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥))
18	17	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑠 = 𝑟 → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))
19	18	oveq2d 6565	. . . . . . 7 ⊢ (𝑠 = 𝑟 → (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥))))
20	19	fveq1d 6105	. . . . . 6 ⊢ (𝑠 = 𝑟 → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘))
21		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑠 = 𝑟 → (𝐷‘𝑠) = (𝐷‘𝑟))
22	21	fveq1d 6105	. . . . . . . . 9 ⊢ (𝑠 = 𝑟 → ((𝐷‘𝑠)‘𝑘) = ((𝐷‘𝑟)‘𝑘))
23	22	sumeq1d 14279	. . . . . . . 8 ⊢ (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
24		prodeq1 14478	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑟 → ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡)) = ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡)))
25	24	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑠 = 𝑟 → ((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))))
26		prodeq1 14478	. . . . . . . . . 10 ⊢ (𝑠 = 𝑟 → ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))
27	25, 26	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑠 = 𝑟 → (((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
28	27	sumeq2ad 38632	. . . . . . . 8 ⊢ (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
29	23, 28	eqtrd 2644	. . . . . . 7 ⊢ (𝑠 = 𝑟 → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
30	29	mpteq2dv 4673	. . . . . 6 ⊢ (𝑠 = 𝑟 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
31	20, 30	eqeq12d 2625	. . . . 5 ⊢ (𝑠 = 𝑟 → (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
32	31	ralbidv 2969	. . . 4 ⊢ (𝑠 = 𝑟 → (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
33		prodeq1 14478	. . . . . . . . 9 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥))
34	33	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))
35	34	oveq2d 6565	. . . . . . 7 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥))))
36	35	fveq1d 6105	. . . . . 6 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘))
37		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (𝐷‘𝑠) = (𝐷‘(𝑟 ∪ {𝑧})))
38	37	fveq1d 6105	. . . . . . . . 9 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ((𝐷‘𝑠)‘𝑘) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
39	38	sumeq1d 14279	. . . . . . . 8 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
40		prodeq1 14478	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡)) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡)))
41	40	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))))
42		prodeq1 14478	. . . . . . . . . 10 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))
43	41, 42	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
44	43	sumeq2ad 38632	. . . . . . . 8 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
45	39, 44	eqtrd 2644	. . . . . . 7 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
46	45	mpteq2dv 4673	. . . . . 6 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
47	36, 46	eqeq12d 2625	. . . . 5 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
48	47	ralbidv 2969	. . . 4 ⊢ (𝑠 = (𝑟 ∪ {𝑧}) → (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
49		prodeq1 14478	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥) = ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥))
50	49	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥)))
51		dvnprodlem3.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥))
52	51	a1i 11	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥)))
53	52	eqcomd 2616	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥)) = 𝐹)
54	50, 53	eqtrd 2644	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)) = 𝐹)
55	54	oveq2d 6565	. . . . . . 7 ⊢ (𝑠 = 𝑇 → (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 𝐹))
56	55	fveq1d 6105	. . . . . 6 ⊢ (𝑠 = 𝑇 → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 𝐹)‘𝑘))
57		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → (𝐷‘𝑠) = (𝐷‘𝑇))
58	57	fveq1d 6105	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝐷‘𝑠)‘𝑘) = ((𝐷‘𝑇)‘𝑘))
59	58	sumeq1d 14279	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
60		prodeq1 14478	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑇 → ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡)) = ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡)))
61	60	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → ((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))))
62		prodeq1 14478	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))
63	61, 62	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → (((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
64	63	sumeq2ad 38632	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
65	59, 64	eqtrd 2644	. . . . . . 7 ⊢ (𝑠 = 𝑇 → Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
66	65	mpteq2dv 4673	. . . . . 6 ⊢ (𝑠 = 𝑇 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
67	56, 66	eqeq12d 2625	. . . . 5 ⊢ (𝑠 = 𝑇 → (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 𝐹)‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
68	67	ralbidv 2969	. . . 4 ⊢ (𝑠 = 𝑇 → (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑠 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑠)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑠 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑠 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 𝐹)‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
69		prod0 14512	. . . . . . . . . . . . 13 ⊢ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥) = 1
70	69	mpteq2i 4669	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)) = (𝑥 ∈ 𝑋 ↦ 1)
71	70	oveq2i 6560	. . . . . . . . . . 11 ⊢ (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))
72	71	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1)))
73		id 22	. . . . . . . . . 10 ⊢ (𝑘 = 0 → 𝑘 = 0)
74	72, 73	fveq12d 6109	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘0))
75	74	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘0))
76		dvnprodlem3.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
77		recnprss 23474	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
78	76, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
79		1cnd 9935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℂ)
80		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 ↦ 1) = (𝑥 ∈ 𝑋 ↦ 1)
81	79, 80	fmptd 6292	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 1):𝑋⟶ℂ)
82		1re 9918	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
83	82	rgenw 2908	. . . . . . . . . . . . . . . 16 ⊢ ∀𝑥 ∈ 𝑋 1 ∈ ℝ
84		dmmptg 5549	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 1 ∈ ℝ → dom (𝑥 ∈ 𝑋 ↦ 1) = 𝑋)
85	83, 84	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ dom (𝑥 ∈ 𝑋 ↦ 1) = 𝑋
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 1) = 𝑋)
87	86	feq2d 5944	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 1):dom (𝑥 ∈ 𝑋 ↦ 1)⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ 1):𝑋⟶ℂ))
88	81, 87	mpbird 246	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 1):dom (𝑥 ∈ 𝑋 ↦ 1)⟶ℂ)
89		restsspw 15915	. . . . . . . . . . . . . . 15 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) ⊆ 𝒫 𝑆
90		dvnprodlem3.x	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
91	89, 90	sseldi 3566	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ 𝒫 𝑆)
92		elpwi 4117	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆)
93	91, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
94	86, 93	eqsstrd 3602	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (𝑥 ∈ 𝑋 ↦ 1) ⊆ 𝑆)
95	88, 94	jca 553	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 1):dom (𝑥 ∈ 𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥 ∈ 𝑋 ↦ 1) ⊆ 𝑆))
96		cnex 9896	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
97	96	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ∈ V)
98		elpm2g 7760	. . . . . . . . . . . 12 ⊢ ((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) → ((𝑥 ∈ 𝑋 ↦ 1) ∈ (ℂ ↑_pm 𝑆) ↔ ((𝑥 ∈ 𝑋 ↦ 1):dom (𝑥 ∈ 𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥 ∈ 𝑋 ↦ 1) ⊆ 𝑆)))
99	97, 76, 98	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ 1) ∈ (ℂ ↑_pm 𝑆) ↔ ((𝑥 ∈ 𝑋 ↦ 1):dom (𝑥 ∈ 𝑋 ↦ 1)⟶ℂ ∧ dom (𝑥 ∈ 𝑋 ↦ 1) ⊆ 𝑆)))
100	95, 99	mpbird 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 1) ∈ (ℂ ↑_pm 𝑆))
101		dvn0 23493	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 1) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘0) = (𝑥 ∈ 𝑋 ↦ 1))
102	78, 100, 101	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘0) = (𝑥 ∈ 𝑋 ↦ 1))
103	102	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘0) = (𝑥 ∈ 𝑋 ↦ 1))
104		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
105	104	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝐷‘∅)‘𝑘) = ((𝐷‘∅)‘0))
106		dvnprodlem3.d	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
107	106	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})))
108		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = ∅ → ((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 ∅))
109		elmapfn 7766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) → 𝑥 Fn ∅)
110		fn0 5924	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 Fn ∅ ↔ 𝑥 = ∅)
111	109, 110	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) → 𝑥 = ∅)
112		velsn 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
113	111, 112	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) → 𝑥 ∈ {∅})
114	112	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ {∅} → 𝑥 = ∅)
115		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = ∅ → 𝑥 = ∅)
116		f0 5999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅:∅⟶(0...𝑛)
117		ovex 6577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0...𝑛) ∈ V
118		0ex 4718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∅ ∈ V
119	117, 118	elmap 7772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∅ ∈ ((0...𝑛) ↑_𝑚 ∅) ↔ ∅:∅⟶(0...𝑛))
120	116, 119	mpbir 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∅ ∈ ((0...𝑛) ↑_𝑚 ∅)
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = ∅ → ∅ ∈ ((0...𝑛) ↑_𝑚 ∅))
122	115, 121	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = ∅ → 𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅))
123	114, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ {∅} → 𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅))
124	113, 123	impbii 198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) ↔ 𝑥 ∈ {∅})
125	124	ax-gen 1713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) ↔ 𝑥 ∈ {∅})
126		dfcleq 2604	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((0...𝑛) ↑_𝑚 ∅) = {∅} ↔ ∀𝑥(𝑥 ∈ ((0...𝑛) ↑_𝑚 ∅) ↔ 𝑥 ∈ {∅}))
127	125, 126	mpbir 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0...𝑛) ↑_𝑚 ∅) = {∅}
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = ∅ → ((0...𝑛) ↑_𝑚 ∅) = {∅})
129	108, 128	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = ∅ → ((0...𝑛) ↑_𝑚 𝑠) = {∅})
130		rabeq 3166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑛) ↑_𝑚 𝑠) = {∅} → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
131	129, 130	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
132		sumeq1 14267	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = ∅ → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ ∅ (𝑐‘𝑡))
133	132	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = ∅ → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛))
134	133	rabbidv 3164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = ∅ → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛})
135	131, 134	eqtrd 2644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = ∅ → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛})
136	135	mpteq2dv 4673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = ∅ → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}))
137	136	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 = ∅) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}))
138		0elpw 4760	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 𝑇
139	138	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 𝑇)
140		nn0ex 11175	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ ∈ V
141	140	mptex 6390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}) ∈ V
142	141	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}) ∈ V)
143	107, 137, 139, 142	fvmptd 6197	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷‘∅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}))
144		eqeq2 2621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 0 → (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0))
145	144	rabbidv 3164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0})
146	145	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0})
147		0nn0 11184	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℕ₀
148	147	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℕ₀)
149		p0ex 4779	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
150	149	rabex 4740	. . . . . . . . . . . . . . . . 17 ⊢ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} ∈ V
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} ∈ V)
152	143, 146, 148, 151	fvmptd 6197	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0})
153	152	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝐷‘∅)‘0) = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0})
154		snidg 4153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∈ V → ∅ ∈ {∅})
155	118, 154	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ {∅}
156		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = 0
157	155, 156	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ {∅} ∧ 0 = 0)
158		sum0 14299	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0
159	158	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = ∅ → Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0)
160	159	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = ∅ → (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0 ↔ 0 = 0))
161	160	elrab 3331	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} ↔ (∅ ∈ {∅} ∧ 0 = 0))
162	157, 161	mpbir 220	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0}
163	162	n0ii 3881	. . . . . . . . . . . . . . . . 17 ⊢ ¬ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = ∅
164		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0}
165		rabrsn 4203	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} → ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {∅}))
166	164, 165	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = ∅ ∨ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {∅})
167	163, 166	mtpor 1686	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {∅}
168	167	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = {∅})
169		iftrue 4042	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → if(𝑘 = 0, {∅}, ∅) = {∅})
170	169	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 = 0) → if(𝑘 = 0, {∅}, ∅) = {∅})
171	168, 170	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 = 0) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0} = if(𝑘 = 0, {∅}, ∅))
172	105, 153, 171	3eqtrd 2648	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝐷‘∅)‘𝑘) = if(𝑘 = 0, {∅}, ∅))
173	172, 170	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝐷‘∅)‘𝑘) = {∅})
174	173	sumeq1d 14279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
175		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
176		fac0 12925	. . . . . . . . . . . . . . . . . . 19 ⊢ (!‘0) = 1
177	176	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → (!‘0) = 1)
178	175, 177	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
179	178	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) = (1 / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))))
180		prod0 14512	. . . . . . . . . . . . . . . . . 18 ⊢ ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡)) = 1
181	180	oveq2i 6560	. . . . . . . . . . . . . . . . 17 ⊢ (1 / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) = (1 / 1)
182		1div1e1 10596	. . . . . . . . . . . . . . . . 17 ⊢ (1 / 1) = 1
183	181, 182	eqtri 2632	. . . . . . . . . . . . . . . 16 ⊢ (1 / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) = 1
184	179, 183	syl6eq 2660	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) = 1)
185		prod0 14512	. . . . . . . . . . . . . . . 16 ⊢ ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = 1
186	185	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = 1)
187	184, 186	oveq12d 6567	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (1 · 1))
188	187	ad2antlr 759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (1 · 1))
189		1t1e1 11052	. . . . . . . . . . . . . 14 ⊢ (1 · 1) = 1
190	189	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (1 · 1) = 1)
191	188, 190	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 = 0) ∧ 𝑐 ∈ {∅}) → (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = 1)
192	191	sumeq2dv 14281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 0) → Σ𝑐 ∈ {∅} (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ {∅}1)
193		ax-1cn 9873	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
194		eqidd 2611	. . . . . . . . . . . . . 14 ⊢ (𝑐 = ∅ → 1 = 1)
195	194	sumsn 14319	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ 1 ∈ ℂ) → Σ𝑐 ∈ {∅}1 = 1)
196	118, 193, 195	mp2an 704	. . . . . . . . . . . 12 ⊢ Σ𝑐 ∈ {∅}1 = 1
197	196	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 0) → Σ𝑐 ∈ {∅}1 = 1)
198	174, 192, 197	3eqtrd 2648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = 0) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = 1)
199	198	mpteq2dv 4673	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ 1))
200	199	eqcomd 2616	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑥 ∈ 𝑋 ↦ 1) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
201	75, 103, 200	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 0) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
202	201	a1d 25	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
203	71	fveq1i 6104	. . . . . . . . 9 ⊢ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘𝑘)
204	203	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘𝑘))
205	76	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑆 ∈ {ℝ, ℂ})
206	205	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
207	90	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑘 = 0) → 𝑋 ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
208	207	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
209	193	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
210		elfznn0 12302	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
211	210	adantl 481	. . . . . . . . . . . 12 ⊢ ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ₀)
212		neqne 2790	. . . . . . . . . . . . 13 ⊢ (¬ 𝑘 = 0 → 𝑘 ≠ 0)
213	212	adantr 480	. . . . . . . . . . . 12 ⊢ ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≠ 0)
214	211, 213	jca 553	. . . . . . . . . . 11 ⊢ ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → (𝑘 ∈ ℕ₀ ∧ 𝑘 ≠ 0))
215		elnnne0 11183	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ₀ ∧ 𝑘 ≠ 0))
216	214, 215	sylibr 223	. . . . . . . . . 10 ⊢ ((¬ 𝑘 = 0 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
217	216	adantll 746	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
218	206, 208, 209, 217	dvnmptconst 38831	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ 1))‘𝑘) = (𝑥 ∈ 𝑋 ↦ 0))
219	143	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝐷‘∅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛}))
220		eqeq2 2621	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘))
221	220	rabbidv 3164	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘})
222	221	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘})
223		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘 → 𝑘 = 𝑘)
224		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘)
225	224	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘 → 𝑘 = Σ𝑡 ∈ ∅ (𝑐‘𝑡))
226	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘 → Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 0)
227	223, 225, 226	3eqtrd 2648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘 → 𝑘 = 0)
228	227	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ {∅} ∧ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘) → 𝑘 = 0)
229	228	adantll 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘) → 𝑘 = 0)
230		simpll 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) ∧ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘) → ¬ 𝑘 = 0)
231	229, 230	pm2.65da 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ 𝑘 = 0 ∧ 𝑐 ∈ {∅}) → ¬ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘)
232	231	ralrimiva 2949	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑘 = 0 → ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘)
233		rabeq0 3911	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘} = ∅ ↔ ∀𝑐 ∈ {∅} ¬ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘)
234	232, 233	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑘 = 0 → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘} = ∅)
235	234	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑘} = ∅)
236	222, 235	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑘 = 0 ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = ∅)
237	236	adantll 746	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = ∅)
238	237	adantlr 747	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ {∅} ∣ Σ𝑡 ∈ ∅ (𝑐‘𝑡) = 𝑛} = ∅)
239	210	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ₀)
240	118	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ∅ ∈ V)
241	219, 238, 239, 240	fvmptd 6197	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐷‘∅)‘𝑘) = ∅)
242	241	sumeq1d 14279	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
243		sum0 14299	. . . . . . . . . . 11 ⊢ Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = 0
244	243	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑐 ∈ ∅ (((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = 0)
245	242, 244	eqtr2d 2645	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → 0 = Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
246	245	mpteq2dv 4673	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ 𝑋 ↦ 0) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
247	204, 218, 246	3eqtrd 2648	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑘 = 0) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
248	247	ex 449	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑘 = 0) → (𝑘 ∈ (0...𝑁) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
249	202, 248	pm2.61dan 828	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
250	249	ralrimiv 2948	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ ∅ ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘∅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ ∅ (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ ∅ (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
251		simpll 786	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))))
252		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝐻‘𝑡)‘𝑥) = ((𝐻‘𝑡)‘𝑦))
253	252	prodeq2ad 38659	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥) = ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑦))
254		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → (𝐻‘𝑡) = (𝐻‘𝑢))
255	254	fveq1d 6105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑢 → ((𝐻‘𝑡)‘𝑦) = ((𝐻‘𝑢)‘𝑦))
256	255	cbvprodv 14485	. . . . . . . . . . . . . . . . 17 ⊢ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑦) = ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)
257	256	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑦) = ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦))
258	253, 257	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥) = ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦))
259	258	cbvmptv 4678	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)) = (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦))
260	259	oveq2i 6560	. . . . . . . . . . . . 13 ⊢ (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥))) = (𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))
261	260	fveq1i 6104	. . . . . . . . . . . 12 ⊢ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = ((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘)
262		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑢 → (𝑐‘𝑡) = (𝑐‘𝑢))
263	262	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → (!‘(𝑐‘𝑡)) = (!‘(𝑐‘𝑢)))
264	263	cbvprodv 14485	. . . . . . . . . . . . . . . . . 18 ⊢ ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡)) = ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))
265	264	oveq2i 6560	. . . . . . . . . . . . . . . . 17 ⊢ ((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢)))
266	265	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))))
267		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑦))
268	267	prodeq2ad 38659	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑦))
269	254	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑢 → (𝑆 D^𝑛 (𝐻‘𝑡)) = (𝑆 D^𝑛 (𝐻‘𝑢)))
270	269, 262	fveq12d 6109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑢 → ((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡)) = ((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢)))
271	270	fveq1d 6105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑢 → (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑦) = (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦))
272	271	cbvprodv 14485	. . . . . . . . . . . . . . . . . 18 ⊢ ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑦) = ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)
273	272	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑦) = ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦))
274	268, 273	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥) = ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦))
275	266, 274	oveq12d 6567	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)))
276	275	sumeq2ad 38632	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)))
277		fveq1 6102	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑢) = (𝑑‘𝑢))
278	277	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (!‘(𝑐‘𝑢)) = (!‘(𝑑‘𝑢)))
279	278	prodeq2ad 38659	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑑 → ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢)) = ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢)))
280	279	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑑 → ((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) = ((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))))
281	277	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → ((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢)) = ((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢)))
282	281	fveq1d 6105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑑 → (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦) = (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))
283	282	prodeq2ad 38659	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑑 → ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦) = ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))
284	280, 283	oveq12d 6567	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → (((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)) = (((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))
285	284	cbvsumv 14274	. . . . . . . . . . . . . . 15 ⊢ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))
286	285	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑐‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑐‘𝑢))‘𝑦)) = Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))
287	276, 286	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))
288	287	cbvmptv 4678	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))
289	261, 288	eqeq12i 2624	. . . . . . . . . . 11 ⊢ (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))))
290	289	ralbii 2963	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))))
291	290	biimpi 205	. . . . . . . . 9 ⊢ (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))))
292	291	ad2antlr 759	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))))
293		simpr 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
294	76	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ})
295	90	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
296		dvnprodlem3.t	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ Fin)
297	296	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ Fin)
298		simp-4l 802	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 𝜑)
299		simpr 476	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
300		dvnprodlem3.h	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ)
301	298, 299, 300	syl2anc 691	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ)
302		dvnprodlem3.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
303	302	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ ℕ₀)
304		simplll 794	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
305	304	3ad2ant1 1075	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → 𝜑)
306		simp2 1055	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → 𝑡 ∈ 𝑇)
307		simp3 1056	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → ℎ ∈ (0...𝑁))
308		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑗 = ℎ → (𝑗 ∈ (0...𝑁) ↔ ℎ ∈ (0...𝑁)))
309	308	3anbi3d 1397	. . . . . . . . . . . 12 ⊢ (𝑗 = ℎ → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁))))
310		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑗 = ℎ → ((𝑆 D^𝑛 (𝐻‘𝑡))‘𝑗) = ((𝑆 D^𝑛 (𝐻‘𝑡))‘ℎ))
311	310	feq1d 5943	. . . . . . . . . . . 12 ⊢ (𝑗 = ℎ → (((𝑆 D^𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D^𝑛 (𝐻‘𝑡))‘ℎ):𝑋⟶ℂ))
312	309, 311	imbi12d 333	. . . . . . . . . . 11 ⊢ (𝑗 = ℎ → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘ℎ):𝑋⟶ℂ)))
313		dvnprodlem3.dvnh	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ)
314	312, 313	chvarv 2251	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘ℎ):𝑋⟶ℂ)
315	305, 306, 307, 314	syl3anc 1318	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝐻‘𝑡))‘ℎ):𝑋⟶ℂ)
316		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) → 𝑟 ⊆ 𝑇)
317	316	ad2antrr 758	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑟 ⊆ 𝑇)
318		simprr 792	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) → 𝑧 ∈ (𝑇 ∖ 𝑟))
319	318	ad2antrr 758	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑧 ∈ (𝑇 ∖ 𝑟))
320	260	eqcomi 2619	. . . . . . . . . . . . . . 15 ⊢ (𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))
321	320	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦))) = (𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥))))
322		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → 𝑘 = 𝑙)
323	321, 322	fveq12d 6109	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑙))
324	288	eqcomi 2619	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
325	324	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
326		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → (!‘𝑘) = (!‘𝑙))
327	326	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) = ((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))))
328	327	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
329	328	sumeq2ad 38632	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
330		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((𝐷‘𝑟)‘𝑘) = ((𝐷‘𝑟)‘𝑙))
331	330	sumeq1d 14279	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
332	329, 331	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
333	332	mpteq2dv 4673	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
334	325, 333	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
335	323, 334	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) ↔ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑙) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
336	335	cbvralv 3147	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) ↔ ∀𝑙 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑙) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
337	336	biimpi 205	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦))) → ∀𝑙 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑙) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
338	337	ad2antlr 759	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑙 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑙) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑙)(((!‘𝑙) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
339		simpr 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
340		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑐 → (𝑑‘𝑧) = (𝑐‘𝑧))
341	340	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑗 − (𝑑‘𝑧)) = (𝑗 − (𝑐‘𝑧)))
342		reseq1 5311	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑑 ↾ 𝑟) = (𝑐 ↾ 𝑟))
343	341, 342	opeq12d 4348	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → ⟨(𝑗 − (𝑑‘𝑧)), (𝑑 ↾ 𝑟)⟩ = ⟨(𝑗 − (𝑐‘𝑧)), (𝑐 ↾ 𝑟)⟩)
344	343	cbvmptv 4678	. . . . . . . . 9 ⊢ (𝑑 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑑‘𝑧)), (𝑑 ↾ 𝑟)⟩) = (𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) ↦ ⟨(𝑗 − (𝑐‘𝑧)), (𝑐 ↾ 𝑟)⟩)
345	294, 295, 297, 301, 303, 315, 106, 317, 319, 338, 339, 344	dvnprodlem2 38837	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑦 ∈ 𝑋 ↦ ∏𝑢 ∈ 𝑟 ((𝐻‘𝑢)‘𝑦)))‘𝑘) = (𝑦 ∈ 𝑋 ↦ Σ𝑑 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑢 ∈ 𝑟 (!‘(𝑑‘𝑢))) · ∏𝑢 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑢))‘(𝑑‘𝑢))‘𝑦)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
346	251, 292, 293, 345	syl21anc 1317	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
347	346	ralrimiva 2949	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) → ∀𝑗 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
348		fveq2 6103	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘))
349		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘))
350	349	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → ((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) = ((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))))
351	350	oveq1d 6564	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
352	351	sumeq2ad 38632	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
353		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗) = ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘))
354	353	sumeq1d 14279	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
355	352, 354	eqtrd 2644	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
356	355	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
357	348, 356	eqeq12d 2625	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
358	357	cbvralv 3147	. . . . . 6 ⊢ (∀𝑗 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑗)(((!‘𝑗) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
359	347, 358	sylib 207	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) ∧ ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
360	359	ex 449	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ (𝑇 ∖ 𝑟))) → (∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑟 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑟)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑟 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑟 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑟 ∪ {𝑧})((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘(𝑟 ∪ {𝑧}))‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ (𝑟 ∪ {𝑧})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑟 ∪ {𝑧})(((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
361	16, 32, 48, 68, 250, 360, 296	findcard2d 8087	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 𝐹)‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
362		nn0uz 11598	. . . . 5 ⊢ ℕ₀ = (ℤ_≥‘0)
363	302, 362	syl6eleq 2698	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
364		eluzfz2 12220	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
365	363, 364	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
366		fveq2 6103	. . . . 5 ⊢ (𝑘 = 𝑁 → ((𝑆 D^𝑛 𝐹)‘𝑘) = ((𝑆 D^𝑛 𝐹)‘𝑁))
367		fveq2 6103	. . . . . . . 8 ⊢ (𝑘 = 𝑁 → ((𝐷‘𝑇)‘𝑘) = ((𝐷‘𝑇)‘𝑁))
368	367	sumeq1d 14279	. . . . . . 7 ⊢ (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
369		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁))
370	369	oveq1d 6564	. . . . . . . . 9 ⊢ (𝑘 = 𝑁 → ((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) = ((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))))
371	370	oveq1d 6564	. . . . . . . 8 ⊢ (𝑘 = 𝑁 → (((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = (((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
372	371	sumeq2ad 38632	. . . . . . 7 ⊢ (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
373	368, 372	eqtrd 2644	. . . . . 6 ⊢ (𝑘 = 𝑁 → Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
374	373	mpteq2dv 4673	. . . . 5 ⊢ (𝑘 = 𝑁 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
375	366, 374	eqeq12d 2625	. . . 4 ⊢ (𝑘 = 𝑁 → (((𝑆 D^𝑛 𝐹)‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ↔ ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))))
376	375	rspccva 3281	. . 3 ⊢ ((∀𝑘 ∈ (0...𝑁)((𝑆 D^𝑛 𝐹)‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) ∧ 𝑁 ∈ (0...𝑁)) → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
377	361, 365, 376	syl2anc 691	. 2 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
378		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑇 → ((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 𝑇))
379		rabeq 3166	. . . . . . . . . . 11 ⊢ (((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 𝑇) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
380	378, 379	syl 17	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
381		sumeq1 14267	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑇 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑇 (𝑐‘𝑡))
382	381	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑇 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛))
383	382	rabbidv 3164	. . . . . . . . . 10 ⊢ (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛})
384	380, 383	eqtrd 2644	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛})
385	384	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}))
386	385	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 = 𝑇) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}))
387		pwidg 4121	. . . . . . . 8 ⊢ (𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇)
388	296, 387	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑇)
389	140	mptex 6390	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) ∈ V
390	389	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}) ∈ V)
391	107, 386, 388, 390	fvmptd 6197	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑇) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}))
392		dvnprodlem3.c	. . . . . . 7 ⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛})
393	392	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛}))
394	391, 393	eqtr4d 2647	. . . . 5 ⊢ (𝜑 → (𝐷‘𝑇) = 𝐶)
395	394	fveq1d 6105	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑇)‘𝑁) = (𝐶‘𝑁))
396	395	sumeq1d 14279	. . 3 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))
397	396	mpteq2dv 4673	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐷‘𝑇)‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
398	377, 397	eqtrd 2644	1 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D^𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 ∀wal 1473 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 {crab 2900 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ⊆ wss 3540 ∅c0 3874 ifcif 4036 𝒫 cpw 4108 {csn 4125 {cpr 4127 ⟨cop 4131 ↦ cmpt 4643 dom cdm 5038 ↾ cres 5040 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↑_𝑚 cmap 7744 ↑_pm cpm 7745 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 · cmul 9820 − cmin 10145 / cdiv 10563 ℕcn 10897 ℕ₀cn0 11169 ℤ_≥cuz 11563 ...cfz 12197 !cfa 12922 Σcsu 14264 ∏cprod 14474 ↾_t crest 15904 TopOpenctopn 15905 ℂ_fldccnfld 19567 D^𝑛 cdvn 23434

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-seq 12664 df-exp 12723 df-fac 12923 df-bc 12952 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265 df-prod 14475 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-fbas 19564 df-fg 19565 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cld 20633 df-ntr 20634 df-cls 20635 df-nei 20712 df-lp 20750 df-perf 20751 df-cn 20841 df-cnp 20842 df-haus 20929 df-tx 21175 df-hmeo 21368 df-fil 21460 df-fm 21552 df-flim 21553 df-flf 21554 df-xms 21935 df-ms 21936 df-tms 21937 df-cncf 22489 df-limc 23436 df-dv 23437 df-dvn 23438

This theorem is referenced by: dvnprod 38839

W3C validator