dvnprod

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

	Ref	Expression
Hypotheses	dvnprod.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvnprod.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
	dvnprod.t	⊢ ( 𝜑 → 𝑇 ∈ Fin )
	dvnprod.h	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) : 𝑋 ⟶ ℂ )
	dvnprod.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	dvnprod.dvnh	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
	dvnprod.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
	dvnprod.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
Assertion	dvnprod	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvnprod.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvnprod.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
3		dvnprod.t	⊢ ( 𝜑 → 𝑇 ∈ Fin )
4		dvnprod.h	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) : 𝑋 ⟶ ℂ )
5		dvnprod.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
6		dvnprod.dvnh	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
7		dvnprod.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑡 ∈ 𝑇 ( ( 𝐻 ‘ 𝑡 ) ‘ 𝑥 ) )
8		dvnprod.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } )
9		fveq2	⊢ ( 𝑢 = 𝑡 → ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑡 ) )
10	9	cbvsumv	⊢ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 )
11	10	eqeq1i	⊢ ( Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 ↔ Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 ) = 𝑚 )
12	11	rabbii	⊢ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } = { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 ) = 𝑚 }
13		fveq1	⊢ ( 𝑑 = 𝑒 → ( 𝑑 ‘ 𝑡 ) = ( 𝑒 ‘ 𝑡 ) )
14	13	sumeq2sdv	⊢ ( 𝑑 = 𝑒 → Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 ) = Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) )
15	14	eqeq1d	⊢ ( 𝑑 = 𝑒 → ( Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 ) = 𝑚 ↔ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 ) )
16	15	cbvrabv	⊢ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑑 ‘ 𝑡 ) = 𝑚 } = { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 }
17	12 16	eqtri	⊢ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } = { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 }
18	17	mpteq2i	⊢ ( 𝑚 ∈ ℕ₀ ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } ) = ( 𝑚 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 } )
19		eqeq2	⊢ ( 𝑚 = 𝑛 → ( Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 ↔ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 ) )
20	19	rabbidv	⊢ ( 𝑚 = 𝑛 → { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 } = { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
21		oveq2	⊢ ( 𝑚 = 𝑛 → ( 0 ... 𝑚 ) = ( 0 ... 𝑛 ) )
22	21	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) = ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) )
23		rabeq	⊢ ( ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) = ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) → { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
24	22 23	syl	⊢ ( 𝑚 = 𝑛 → { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
25	20 24	eqtrd	⊢ ( 𝑚 = 𝑛 → { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
26	25	cbvmptv	⊢ ( 𝑚 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
27	18 26	eqtri	⊢ ( 𝑚 ∈ ℕ₀ ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
28	27	mpteq2i	⊢ ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑚 ∈ ℕ₀ ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } ) ) = ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) )
29		sumeq1	⊢ ( 𝑟 = 𝑠 → Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) )
30	29	eqeq1d	⊢ ( 𝑟 = 𝑠 → ( Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 ) )
31	30	rabbidv	⊢ ( 𝑟 = 𝑠 → { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
32		oveq2	⊢ ( 𝑟 = 𝑠 → ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) = ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) )
33		rabeq	⊢ ( ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) = ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) → { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
34	32 33	syl	⊢ ( 𝑟 = 𝑠 → { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
35	31 34	eqtrd	⊢ ( 𝑟 = 𝑠 → { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
36	35	mpteq2dv	⊢ ( 𝑟 = 𝑠 → ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) )
37	36	cbvmptv	⊢ ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑟 ) ∣ Σ 𝑡 ∈ 𝑟 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) ) = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) )
38	28 37	eqtri	⊢ ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑚 ∈ ℕ₀ ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑_m 𝑟 ) ∣ Σ 𝑢 ∈ 𝑟 ( 𝑑 ‘ 𝑢 ) = 𝑚 } ) ) = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑒 ‘ 𝑡 ) = 𝑛 } ) )
39		fveq1	⊢ ( 𝑐 = 𝑒 → ( 𝑐 ‘ 𝑡 ) = ( 𝑒 ‘ 𝑡 ) )
40	39	sumeq2sdv	⊢ ( 𝑐 = 𝑒 → Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = Σ 𝑡 ∈ 𝑇 ( 𝑒 ‘ 𝑡 ) )
41	40	eqeq1d	⊢ ( 𝑐 = 𝑒 → ( Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ 𝑇 ( 𝑒 ‘ 𝑡 ) = 𝑛 ) )
42	41	cbvrabv	⊢ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑒 ‘ 𝑡 ) = 𝑛 }
43	42	mpteq2i	⊢ ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
44	8 43	eqtri	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑_m 𝑇 ) ∣ Σ 𝑡 ∈ 𝑇 ( 𝑒 ‘ 𝑡 ) = 𝑛 } )
45	1 2 3 4 5 6 7 38 44	dvnprodlem3	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
46		fveq1	⊢ ( 𝑒 = 𝑐 → ( 𝑒 ‘ 𝑡 ) = ( 𝑐 ‘ 𝑡 ) )
47	46	fveq2d	⊢ ( 𝑒 = 𝑐 → ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) = ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
48	47	prodeq2ad	⊢ ( 𝑒 = 𝑐 → ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) = ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) )
49	48	oveq2d	⊢ ( 𝑒 = 𝑐 → ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) )
50	46	fveq2d	⊢ ( 𝑒 = 𝑐 → ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) = ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) )
51	50	fveq1d	⊢ ( 𝑒 = 𝑐 → ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
52	51	prodeq2ad	⊢ ( 𝑒 = 𝑐 → ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
53	49 52	oveq12d	⊢ ( 𝑒 = 𝑐 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
54	53	cbvsumv	⊢ Σ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
55		eqid	⊢ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
56	54 55	eqtri	⊢ Σ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) )
57	56	mpteq2i	⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
58	57	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑒 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑒 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑒 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )
59	45 58	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑡 ∈ 𝑇 ( ! ‘ ( 𝑐 ‘ 𝑡 ) ) ) · ∏ 𝑡 ∈ 𝑇 ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑡 ) ) ‘ ( 𝑐 ‘ 𝑡 ) ) ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem dvnprod

Proof