Theorem dvnprodlem3

Description: The multinomial formula for the k -th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	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	dvnprodlem3	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvnprodlem3.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvnprodlem3.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		dvnprodlem3.t	⊢ ( 𝜑 → 𝑇 ∈ Fin )
4		dvnprodlem3.h	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) : 𝑋 ⟶ ℂ )
5		dvnprodlem3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		dvnprodlem3.dvnh	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ )
7		dvnprodlem3.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
8		dvnprodlem3.d	⊢ 𝐷 = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
9		dvnprodlem3.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
10		prodeq1	⊢ ( 𝑠 = ∅ → ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
11	10	mpteq2dv	⊢ ( 𝑠 = ∅ → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
12	11	oveq2d	⊢ ( 𝑠 = ∅ → ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) )
13	12	fveq1d	⊢ ( 𝑠 = ∅ → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
14		fveq2	⊢ ( 𝑠 = ∅ → ( 𝐷 ‘ 𝑠 ) = ( 𝐷 ‘ ∅ ) )
15	14	fveq1d	⊢ ( 𝑠 = ∅ → ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) )
16	15	sumeq1d	⊢ ( 𝑠 = ∅ → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
17		prodeq1	⊢ ( 𝑠 = ∅ → ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
18	17	oveq2d	⊢ ( 𝑠 = ∅ → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
19		prodeq1	⊢ ( 𝑠 = ∅ → ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
20	18 19	oveq12d	⊢ ( 𝑠 = ∅ → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
21	20	sumeq2sdv	⊢ ( 𝑠 = ∅ → Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
22	16 21	eqtrd	⊢ ( 𝑠 = ∅ → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
23	22	mpteq2dv	⊢ ( 𝑠 = ∅ → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
24	13 23	eqeq12d	⊢ ( 𝑠 = ∅ → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
25	24	ralbidv	⊢ ( 𝑠 = ∅ → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
26		prodeq1	⊢ ( 𝑠 = 𝑟 → ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
27	26	mpteq2dv	⊢ ( 𝑠 = 𝑟 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
28	27	oveq2d	⊢ ( 𝑠 = 𝑟 → ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) )
29	28	fveq1d	⊢ ( 𝑠 = 𝑟 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
30		fveq2	⊢ ( 𝑠 = 𝑟 → ( 𝐷 ‘ 𝑠 ) = ( 𝐷 ‘ 𝑟 ) )
31	30	fveq1d	⊢ ( 𝑠 = 𝑟 → ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) )
32	31	sumeq1d	⊢ ( 𝑠 = 𝑟 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
33		prodeq1	⊢ ( 𝑠 = 𝑟 → ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
34	33	oveq2d	⊢ ( 𝑠 = 𝑟 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
35		prodeq1	⊢ ( 𝑠 = 𝑟 → ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
36	34 35	oveq12d	⊢ ( 𝑠 = 𝑟 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
37	36	sumeq2sdv	⊢ ( 𝑠 = 𝑟 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
38	32 37	eqtrd	⊢ ( 𝑠 = 𝑟 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
39	38	mpteq2dv	⊢ ( 𝑠 = 𝑟 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
40	29 39	eqeq12d	⊢ ( 𝑠 = 𝑟 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
41	40	ralbidv	⊢ ( 𝑠 = 𝑟 → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
42		prodeq1	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
43	42	mpteq2dv	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
44	43	oveq2d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) )
45	44	fveq1d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
46		fveq2	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( 𝐷 ‘ 𝑠 ) = ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) )
47	46	fveq1d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) )
48	47	sumeq1d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
49		prodeq1	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
50	49	oveq2d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
51		prodeq1	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
52	50 51	oveq12d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
53	52	sumeq2sdv	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
54	48 53	eqtrd	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
55	54	mpteq2dv	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
56	45 55	eqeq12d	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
57	56	ralbidv	⊢ ( 𝑠 = ( 𝑟 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
58		prodeq1	⊢ ( 𝑠 = 𝑇 → ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
59	58	mpteq2dv	⊢ ( 𝑠 = 𝑇 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
60	7	a1i	⊢ ( 𝑠 = 𝑇 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
61	60	eqcomd	⊢ ( 𝑠 = 𝑇 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = 𝐹 )
62	59 61	eqtrd	⊢ ( 𝑠 = 𝑇 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = 𝐹 )
63	62	oveq2d	⊢ ( 𝑠 = 𝑇 → ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 𝐹 ) )
64	63	fveq1d	⊢ ( 𝑠 = 𝑇 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
65		fveq2	⊢ ( 𝑠 = 𝑇 → ( 𝐷 ‘ 𝑠 ) = ( 𝐷 ‘ 𝑇 ) )
66	65	fveq1d	⊢ ( 𝑠 = 𝑇 → ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) )
67	66	sumeq1d	⊢ ( 𝑠 = 𝑇 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
68		prodeq1	⊢ ( 𝑠 = 𝑇 → ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
69	68	oveq2d	⊢ ( 𝑠 = 𝑇 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
70		prodeq1	⊢ ( 𝑠 = 𝑇 → ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
71	69 70	oveq12d	⊢ ( 𝑠 = 𝑇 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
72	71	sumeq2sdv	⊢ ( 𝑠 = 𝑇 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
73	67 72	eqtrd	⊢ ( 𝑠 = 𝑇 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
74	73	mpteq2dv	⊢ ( 𝑠 = 𝑇 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
75	64 74	eqeq12d	⊢ ( 𝑠 = 𝑇 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
76	75	ralbidv	⊢ ( 𝑠 = 𝑇 → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑠 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑠 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑠 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑠 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
77		prod0	⊢ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = 1
78	77	mpteq2i	⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ 1 )
79	78	oveq2i	⊢ ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) )
80	79	a1i	⊢ ( 𝑘 = 0 → ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) )
81		id	⊢ ( 𝑘 = 0 → 𝑘 = 0 )
82	80 81	fveq12d	⊢ ( 𝑘 = 0 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 0 ) )
83	82	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 0 ) )
84		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
85	1 84	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
86		1cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℂ )
87	86	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 1 ) : 𝑋 ⟶ ℂ )
88		1re	⊢ 1 ∈ ℝ
89	88	rgenw	⊢ ∀ 𝑥 ∈ 𝑋 1 ∈ ℝ
90		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 1 ∈ ℝ → dom ( 𝑥 ∈ 𝑋 ↦ 1 ) = 𝑋 )
91	89 90	ax-mp	⊢ dom ( 𝑥 ∈ 𝑋 ↦ 1 ) = 𝑋
92	91	a1i	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 1 ) = 𝑋 )
93	92	feq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 1 ) : dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 1 ) : 𝑋 ⟶ ℂ ) )
94	87 93	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 1 ) : dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⟶ ℂ )
95		restsspw	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ⊆ 𝒫 𝑆
96	95 2	sseldi	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑆 )
97		elpwi	⊢ ( 𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆 )
98	96 97	syl	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
99	92 98	eqsstrd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⊆ 𝑆 )
100	94 99	jca	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 1 ) : dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⟶ ℂ ∧ dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⊆ 𝑆 ) )
101		cnex	⊢ ℂ ∈ V
102	101	a1i	⊢ ( 𝜑 → ℂ ∈ V )
103		elpm2g	⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( ( 𝑥 ∈ 𝑋 ↦ 1 ) ∈ ( ℂ ↑pm 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ 1 ) : dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⟶ ℂ ∧ dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⊆ 𝑆 ) ) )
104	102 1 103	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 1 ) ∈ ( ℂ ↑pm 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ 1 ) : dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⟶ ℂ ∧ dom ( 𝑥 ∈ 𝑋 ↦ 1 ) ⊆ 𝑆 ) ) )
105	100 104	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 1 ) ∈ ( ℂ ↑pm 𝑆 ) )
106		dvn0	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ 1 ) ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ 1 ) )
107	85 105 106	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ 1 ) )
108	107	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ 1 ) )
109		fveq2	⊢ ( 𝑘 = 0 → ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) = ( ( 𝐷 ‘ ∅ ) ‘ 0 ) )
110	109	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) = ( ( 𝐷 ‘ ∅ ) ‘ 0 ) )
111		oveq2	⊢ ( 𝑠 = ∅ → ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m ∅ ) )
112		elmapfn	⊢ ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) → 𝑥 Fn ∅ )
113		fn0	⊢ ( 𝑥 Fn ∅ ↔ 𝑥 = ∅ )
114	112 113	sylib	⊢ ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) → 𝑥 = ∅ )
115		velsn	⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
116	114 115	sylibr	⊢ ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) → 𝑥 ∈ { ∅ } )
117	115	biimpi	⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
118		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
119		f0	⊢ ∅ : ∅ ⟶ ( 0 ... 𝑛 )
120		ovex	⊢ ( 0 ... 𝑛 ) ∈ V
121		0ex	⊢ ∅ ∈ V
122	120 121	elmap	⊢ ( ∅ ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) ↔ ∅ : ∅ ⟶ ( 0 ... 𝑛 ) )
123	119 122	mpbir	⊢ ∅ ∈ ( ( 0 ... 𝑛 ) ↑m ∅ )
124	123	a1i	⊢ ( 𝑥 = ∅ → ∅ ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) )
125	118 124	eqeltrd	⊢ ( 𝑥 = ∅ → 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) )
126	117 125	syl	⊢ ( 𝑥 ∈ { ∅ } → 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) )
127	116 126	impbii	⊢ ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) ↔ 𝑥 ∈ { ∅ } )
128	127	ax-gen	⊢ ∀ 𝑥 ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) ↔ 𝑥 ∈ { ∅ } )
129		dfcleq	⊢ ( ( ( 0 ... 𝑛 ) ↑m ∅ ) = { ∅ } ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 0 ... 𝑛 ) ↑m ∅ ) ↔ 𝑥 ∈ { ∅ } ) )
130	128 129	mpbir	⊢ ( ( 0 ... 𝑛 ) ↑m ∅ ) = { ∅ }
131	130	a1i	⊢ ( 𝑠 = ∅ → ( ( 0 ... 𝑛 ) ↑m ∅ ) = { ∅ } )
132	111 131	eqtrd	⊢ ( 𝑠 = ∅ → ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = { ∅ } )
133		rabeq	⊢ ( ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = { ∅ } → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
134	132 133	syl	⊢ ( 𝑠 = ∅ → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
135		sumeq1	⊢ ( 𝑠 = ∅ → Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) )
136	135	eqeq1d	⊢ ( 𝑠 = ∅ → ( Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 ) )
137	136	rabbidv	⊢ ( 𝑠 = ∅ → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
138	134 137	eqtrd	⊢ ( 𝑠 = ∅ → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
139	138	mpteq2dv	⊢ ( 𝑠 = ∅ → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
140		0elpw	⊢ ∅ ∈ 𝒫 𝑇
141	140	a1i	⊢ ( 𝜑 → ∅ ∈ 𝒫 𝑇 )
142		nn0ex	⊢ ℕ0 ∈ V
143	142	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) ∈ V
144	143	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) ∈ V )
145	8 139 141 144	fvmptd3	⊢ ( 𝜑 → ( 𝐷 ‘ ∅ ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
146		eqeq2	⊢ ( 𝑛 = 0 → ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 ) )
147	146	rabbidv	⊢ ( 𝑛 = 0 → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } )
148	147	adantl	⊢ ( ( 𝜑 ∧ 𝑛 = 0 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } )
149		0nn0	⊢ 0 ∈ ℕ0
150	149	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
151		p0ex	⊢ { ∅ } ∈ V
152	151	rabex	⊢ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } ∈ V
153	152	a1i	⊢ ( 𝜑 → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } ∈ V )
154	145 148 150 153	fvmptd	⊢ ( 𝜑 → ( ( 𝐷 ‘ ∅ ) ‘ 0 ) = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } )
155	154	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝐷 ‘ ∅ ) ‘ 0 ) = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } )
156		snidg	⊢ ( ∅ ∈ V → ∅ ∈ { ∅ } )
157	121 156	ax-mp	⊢ ∅ ∈ { ∅ }
158		eqid	⊢ 0 = 0
159	157 158	pm3.2i	⊢ ( ∅ ∈ { ∅ } ∧ 0 = 0 )
160		sum0	⊢ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0
161	160	a1i	⊢ ( 𝑐 = ∅ → Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 )
162	161	eqeq1d	⊢ ( 𝑐 = ∅ → ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 ↔ 0 = 0 ) )
163	162	elrab	⊢ ( ∅ ∈ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } ↔ ( ∅ ∈ { ∅ } ∧ 0 = 0 ) )
164	159 163	mpbir	⊢ ∅ ∈ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 }
165	164	n0ii	⊢ ¬ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = ∅
166		eqid	⊢ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 }
167		rabrsn	⊢ ( { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } → ( { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = ∅ ∨ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { ∅ } ) )
168	166 167	ax-mp	⊢ ( { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = ∅ ∨ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { ∅ } )
169	165 168	mtpor	⊢ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { ∅ }
170	169	a1i	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = { ∅ } )
171		iftrue	⊢ ( 𝑘 = 0 → if ( 𝑘 = 0 , { ∅ } , ∅ ) = { ∅ } )
172	171	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → if ( 𝑘 = 0 , { ∅ } , ∅ ) = { ∅ } )
173	170 172	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 } = if ( 𝑘 = 0 , { ∅ } , ∅ ) )
174	110 155 173	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) = if ( 𝑘 = 0 , { ∅ } , ∅ ) )
175	174 172	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) = { ∅ } )
176	175	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ { ∅ } ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
177		fveq2	⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = ( ! ‘ 0 ) )
178		fac0	⊢ ( ! ‘ 0 ) = 1
179	178	a1i	⊢ ( 𝑘 = 0 → ( ! ‘ 0 ) = 1 )
180	177 179	eqtrd	⊢ ( 𝑘 = 0 → ( ! ‘ 𝑘 ) = 1 )
181	180	oveq1d	⊢ ( 𝑘 = 0 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( 1 / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
182		prod0	⊢ ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = 1
183	182	oveq2i	⊢ ( 1 / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( 1 / 1 )
184		1div1e1	⊢ ( 1 / 1 ) = 1
185	183 184	eqtri	⊢ ( 1 / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = 1
186	181 185	eqtrdi	⊢ ( 𝑘 = 0 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = 1 )
187		prod0	⊢ ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = 1
188	187	a1i	⊢ ( 𝑘 = 0 → ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = 1 )
189	186 188	oveq12d	⊢ ( 𝑘 = 0 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( 1 · 1 ) )
190	189	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑘 = 0 ) ∧ 𝑐 ∈ { ∅ } ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( 1 · 1 ) )
191		1t1e1	⊢ ( 1 · 1 ) = 1
192	191	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 = 0 ) ∧ 𝑐 ∈ { ∅ } ) → ( 1 · 1 ) = 1 )
193	190 192	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 = 0 ) ∧ 𝑐 ∈ { ∅ } ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = 1 )
194	193	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → Σ 𝑐 ∈ { ∅ } ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ { ∅ } 1 )
195		ax-1cn	⊢ 1 ∈ ℂ
196		eqidd	⊢ ( 𝑐 = ∅ → 1 = 1 )
197	196	sumsn	⊢ ( ( ∅ ∈ V ∧ 1 ∈ ℂ ) → Σ 𝑐 ∈ { ∅ } 1 = 1 )
198	121 195 197	mp2an	⊢ Σ 𝑐 ∈ { ∅ } 1 = 1
199	198	a1i	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → Σ 𝑐 ∈ { ∅ } 1 = 1 )
200	176 194 199	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = 1 )
201	200	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 1 ) )
202	201	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑥 ∈ 𝑋 ↦ 1 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
203	83 108 202	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
204	203	a1d	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
205	79	fveq1i	⊢ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 𝑘 )
206	205	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 𝑘 ) )
207	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) → 𝑆 ∈ { ℝ , ℂ } )
208	207	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
209	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
210	209	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
211	195	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
212		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
213	212	adantl	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
214		neqne	⊢ ( ¬ 𝑘 = 0 → 𝑘 ≠ 0 )
215	214	adantr	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ≠ 0 )
216	213 215	jca	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0 ) )
217		elnnne0	⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0 ) )
218	216 217	sylibr	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
219	218	adantll	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
220	208 210 211 219	dvnmptconst	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ 1 ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
221	145	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐷 ‘ ∅ ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
222		eqeq2	⊢ ( 𝑛 = 𝑘 → ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 ) )
223	222	rabbidv	⊢ ( 𝑛 = 𝑘 → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 } )
224	223	adantl	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 } )
225		eqidd	⊢ ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 → 𝑘 = 𝑘 )
226		id	⊢ ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 → Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 )
227	226	eqcomd	⊢ ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 → 𝑘 = Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) )
228	160	a1i	⊢ ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 → Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 0 )
229	225 227 228	3eqtrd	⊢ ( Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 → 𝑘 = 0 )
230	229	adantl	⊢ ( ( 𝑐 ∈ { ∅ } ∧ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 ) → 𝑘 = 0 )
231	230	adantll	⊢ ( ( ( ¬ 𝑘 = 0 ∧ 𝑐 ∈ { ∅ } ) ∧ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 ) → 𝑘 = 0 )
232		simpll	⊢ ( ( ( ¬ 𝑘 = 0 ∧ 𝑐 ∈ { ∅ } ) ∧ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 ) → ¬ 𝑘 = 0 )
233	231 232	pm2.65da	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑐 ∈ { ∅ } ) → ¬ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 )
234	233	ralrimiva	⊢ ( ¬ 𝑘 = 0 → ∀ 𝑐 ∈ { ∅ } ¬ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 )
235		rabeq0	⊢ ( { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 } = ∅ ↔ ∀ 𝑐 ∈ { ∅ } ¬ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 )
236	234 235	sylibr	⊢ ( ¬ 𝑘 = 0 → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 } = ∅ )
237	236	adantr	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑘 } = ∅ )
238	224 237	eqtrd	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = ∅ )
239	238	adantll	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = ∅ )
240	239	adantlr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ { ∅ } ∣ Σ 𝑡 ∈ ∅ ( 𝑐 ‘ 𝑡 ) = 𝑛 } = ∅ )
241	212	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
242	121	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ∅ ∈ V )
243	221 240 241 242	fvmptd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) = ∅ )
244	243	sumeq1d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ∅ ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
245		sum0	⊢ Σ 𝑐 ∈ ∅ ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = 0
246	245	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑐 ∈ ∅ ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = 0 )
247	244 246	eqtr2d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 0 = Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
248	247	mpteq2dv	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ 𝑋 ↦ 0 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
249	206 220 248	3eqtrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
250	249	ex	⊢ ( ( 𝜑 ∧ ¬ 𝑘 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
251	204 250	pm2.61dan	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
252	251	ralrimiv	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ∅ ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ∅ ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ∅ ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ∅ ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
253		simpll	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) )
254		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑦 ) )
255	254	prodeq2ad	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑦 ) )
256		fveq2	⊢ ( 𝑡 = 𝑢 → ( 𝐻 ‘ 𝑡 ) = ( 𝐻 ‘ 𝑢 ) )
257	256	fveq1d	⊢ ( 𝑡 = 𝑢 → ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑦 ) = ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) )
258	257	cbvprodv	⊢ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑦 ) = ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 )
259	258	a1i	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑦 ) = ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) )
260	255 259	eqtrd	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) = ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) )
261	260	cbvmptv	⊢ ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) )
262	261	oveq2i	⊢ ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) )
263	262	fveq1i	⊢ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 )
264		fveq2	⊢ ( 𝑡 = 𝑢 → ( 𝑐 ‘ 𝑡 ) = ( 𝑐 ‘ 𝑢 ) )
265	264	fveq2d	⊢ ( 𝑡 = 𝑢 → ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) )
266	265	cbvprodv	⊢ ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) = ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) )
267	266	oveq2i	⊢ ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) )
268	267	a1i	⊢ ( 𝑥 = 𝑦 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) )
269		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑦 ) )
270	269	prodeq2ad	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑦 ) )
271	256	oveq2d	⊢ ( 𝑡 = 𝑢 → ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) = ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) )
272	271 264	fveq12d	⊢ ( 𝑡 = 𝑢 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) )
273	272	fveq1d	⊢ ( 𝑡 = 𝑢 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑦 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) )
274	273	cbvprodv	⊢ ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑦 ) = ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 )
275	274	a1i	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑦 ) = ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) )
276	270 275	eqtrd	⊢ ( 𝑥 = 𝑦 → ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) )
277	268 276	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
278	277	sumeq2sdv	⊢ ( 𝑥 = 𝑦 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
279		fveq1	⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑢 ) )
280	279	fveq2d	⊢ ( 𝑐 = 𝑑 → ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) = ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) )
281	280	prodeq2ad	⊢ ( 𝑐 = 𝑑 → ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) = ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) )
282	281	oveq2d	⊢ ( 𝑐 = 𝑑 → ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) )
283	279	fveq2d	⊢ ( 𝑐 = 𝑑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) = ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) )
284	283	fveq1d	⊢ ( 𝑐 = 𝑑 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) )
285	284	prodeq2ad	⊢ ( 𝑐 = 𝑑 → ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) = ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) )
286	282 285	oveq12d	⊢ ( 𝑐 = 𝑑 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
287	286	cbvsumv	⊢ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) ) = Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) )
288	287	a1i	⊢ ( 𝑥 = 𝑦 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑐 ‘ 𝑢 ) ) ‘ 𝑦 ) ) = Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
289	278 288	eqtrd	⊢ ( 𝑥 = 𝑦 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
290	289	cbvmptv	⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) )
291	263 290	eqeq12i	⊢ ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) )
292	291	ralbii	⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) )
293	292	biimpi	⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) )
294	293	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) )
295		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
296	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
297	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
298	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 ∈ Fin )
299		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
300		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
301	299 300 4	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) : 𝑋 ⟶ ℂ )
302	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
303		simplll	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
304	303	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
305		simp2	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → 𝑡 ∈ 𝑇 )
306		simp3	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → ℎ ∈ ( 0 ... 𝑁 ) )
307		eleq1w	⊢ ( 𝑗 = ℎ → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ℎ ∈ ( 0 ... 𝑁 ) ) )
308	307	3anbi3d	⊢ ( 𝑗 = ℎ → ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) ) )
309		fveq2	⊢ ( 𝑗 = ℎ → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ℎ ) )
310	309	feq1d	⊢ ( 𝑗 = ℎ → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ℎ ) : 𝑋 ⟶ ℂ ) )
311	308 310	imbi12d	⊢ ( 𝑗 = ℎ → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ℎ ) : 𝑋 ⟶ ℂ ) ) )
312	311 6	chvarvv	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ℎ ) : 𝑋 ⟶ ℂ )
313	304 305 306 312	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ 𝑇 ∧ ℎ ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ℎ ) : 𝑋 ⟶ ℂ )
314		simprl	⊢ ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) → 𝑟 ⊆ 𝑇 )
315	314	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑟 ⊆ 𝑇 )
316		simprr	⊢ ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) → 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) )
317	316	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) )
318	262	eqcomi	⊢ ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) )
319	318	a1i	⊢ ( 𝑘 = 𝑙 → ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) = ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) )
320		id	⊢ ( 𝑘 = 𝑙 → 𝑘 = 𝑙 )
321	319 320	fveq12d	⊢ ( 𝑘 = 𝑙 → ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑙 ) )
322	290	eqcomi	⊢ ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
323	322	a1i	⊢ ( 𝑘 = 𝑙 → ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
324		fveq2	⊢ ( 𝑘 = 𝑙 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑙 ) )
325	324	oveq1d	⊢ ( 𝑘 = 𝑙 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
326	325	oveq1d	⊢ ( 𝑘 = 𝑙 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
327	326	sumeq2sdv	⊢ ( 𝑘 = 𝑙 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
328		fveq2	⊢ ( 𝑘 = 𝑙 → ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) )
329	328	sumeq1d	⊢ ( 𝑘 = 𝑙 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
330	327 329	eqtrd	⊢ ( 𝑘 = 𝑙 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
331	330	mpteq2dv	⊢ ( 𝑘 = 𝑙 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
332	323 331	eqtrd	⊢ ( 𝑘 = 𝑙 → ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
333	321 332	eqeq12d	⊢ ( 𝑘 = 𝑙 → ( ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑙 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
334	333	cbvralvw	⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ↔ ∀ 𝑙 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑙 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
335	334	biimpi	⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) → ∀ 𝑙 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑙 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
336	335	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑙 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑙 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑙 ) ( ( ( ! ‘ 𝑙 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
337		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
338		fveq1	⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 𝑧 ) = ( 𝑐 ‘ 𝑧 ) )
339	338	oveq2d	⊢ ( 𝑑 = 𝑐 → ( 𝑗 − ( 𝑑 ‘ 𝑧 ) ) = ( 𝑗 − ( 𝑐 ‘ 𝑧 ) ) )
340		reseq1	⊢ ( 𝑑 = 𝑐 → ( 𝑑 ↾ 𝑟 ) = ( 𝑐 ↾ 𝑟 ) )
341	339 340	opeq12d	⊢ ( 𝑑 = 𝑐 → ⟨ ( 𝑗 − ( 𝑑 ‘ 𝑧 ) ) , ( 𝑑 ↾ 𝑟 ) ⟩ = ⟨ ( 𝑗 − ( 𝑐 ‘ 𝑧 ) ) , ( 𝑐 ↾ 𝑟 ) ⟩ )
342	341	cbvmptv	⊢ ( 𝑑 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ↦ ⟨ ( 𝑗 − ( 𝑑 ‘ 𝑧 ) ) , ( 𝑑 ↾ 𝑟 ) ⟩ ) = ( 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ↦ ⟨ ( 𝑗 − ( 𝑐 ‘ 𝑧 ) ) , ( 𝑐 ↾ 𝑟 ) ⟩ )
343	296 297 298 301 302 313 8 315 317 336 337 342	dvnprodlem2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑦 ∈ 𝑋 ↦ ∏ 𝑢 ∈ 𝑟 ( ( 𝐻 ‘ 𝑢 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑑 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑢 ∈ 𝑟 ( ! ‘ ( 𝑑 ‘ 𝑢 ) ) ) · ∏ 𝑢 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑢 ) ) ‘ ( 𝑑 ‘ 𝑢 ) ) ‘ 𝑦 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
344	253 294 295 343	syl21anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
345	344	ralrimiva	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
346		fveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
347		fveq2	⊢ ( 𝑗 = 𝑘 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑘 ) )
348	347	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
349	348	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
350	349	sumeq2sdv	⊢ ( 𝑗 = 𝑘 → Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
351		fveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) = ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) )
352	351	sumeq1d	⊢ ( 𝑗 = 𝑘 → Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
353	350 352	eqtrd	⊢ ( 𝑗 = 𝑘 → Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
354	353	mpteq2dv	⊢ ( 𝑗 = 𝑘 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
355	346 354	eqeq12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
356	355	cbvralvw	⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑗 ) ( ( ( ! ‘ 𝑗 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
357	345 356	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
358	357	ex	⊢ ( ( 𝜑 ∧ ( 𝑟 ⊆ 𝑇 ∧ 𝑧 ∈ ( 𝑇 ∖ 𝑟 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑟 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑟 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑟 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑟 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ ( 𝑟 ∪ { 𝑧 } ) ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑟 ∪ { 𝑧 } ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
359	25 41 57 76 252 358 3	findcard2d	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
360		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
361	5 360	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
362		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
363	361 362	syl	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
364		fveq2	⊢ ( 𝑘 = 𝑁 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
365		fveq2	⊢ ( 𝑘 = 𝑁 → ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) = ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) )
366	365	sumeq1d	⊢ ( 𝑘 = 𝑁 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
367		fveq2	⊢ ( 𝑘 = 𝑁 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑁 ) )
368	367	oveq1d	⊢ ( 𝑘 = 𝑁 → ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
369	368	oveq1d	⊢ ( 𝑘 = 𝑁 → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
370	369	sumeq2sdv	⊢ ( 𝑘 = 𝑁 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
371	366 370	eqtrd	⊢ ( 𝑘 = 𝑁 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
372	371	mpteq2dv	⊢ ( 𝑘 = 𝑁 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
373	364 372	eqeq12d	⊢ ( 𝑘 = 𝑁 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ) )
374	373	rspccva	⊢ ( ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
375	359 363 374	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
376		oveq2	⊢ ( 𝑠 = 𝑇 → ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m 𝑇 ) )
377		rabeq	⊢ ( ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m 𝑇 ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
378	376 377	syl	⊢ ( 𝑠 = 𝑇 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
379		sumeq1	⊢ ( 𝑠 = 𝑇 → Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) )
380	379	eqeq1d	⊢ ( 𝑠 = 𝑇 → ( Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 ) )
381	380	rabbidv	⊢ ( 𝑠 = 𝑇 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
382	378 381	eqtrd	⊢ ( 𝑠 = 𝑇 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
383	382	mpteq2dv	⊢ ( 𝑠 = 𝑇 → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
384		pwidg	⊢ ( 𝑇 ∈ Fin → 𝑇 ∈ 𝒫 𝑇 )
385	3 384	syl	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝑇 )
386	142	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) ∈ V
387	386	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) ∈ V )
388	8 383 385 387	fvmptd3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑇 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
389	9	a1i	⊢ ( 𝜑 → 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
390	388 389	eqtr4d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑇 ) = 𝐶 )
391	390	fveq1d	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) = ( 𝐶 ‘ 𝑁 ) )
392	391	sumeq1d	⊢ ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
393	392	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐷 ‘ 𝑇 ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
394	375 393	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )