Metamath Proof Explorer


Theorem 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 ( 𝜑𝑁 ∈ ℕ0 )
dvnprod.dvnh ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
dvnprod.f 𝐹 = ( 𝑥𝑋 ↦ ∏ 𝑡𝑇 ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
dvnprod.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 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 ( 𝜑𝑁 ∈ ℕ0 )
6 dvnprod.dvnh ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
7 dvnprod.f 𝐹 = ( 𝑥𝑋 ↦ ∏ 𝑡𝑇 ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
8 dvnprod.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 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 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m 𝑟 ) ∣ Σ 𝑢𝑟 ( 𝑑𝑢 ) = 𝑚 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 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 ↦ { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑m 𝑟 ) ∣ Σ 𝑡𝑟 ( 𝑒𝑡 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑟 ) ∣ Σ 𝑡𝑟 ( 𝑒𝑡 ) = 𝑛 } )
27 18 26 eqtri ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m 𝑟 ) ∣ Σ 𝑢𝑟 ( 𝑑𝑢 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑟 ) ∣ Σ 𝑡𝑟 ( 𝑒𝑡 ) = 𝑛 } )
28 27 mpteq2i ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m 𝑟 ) ∣ Σ 𝑢𝑟 ( 𝑑𝑢 ) = 𝑚 } ) ) = ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 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 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑟 ) ∣ Σ 𝑡𝑟 ( 𝑒𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑒𝑡 ) = 𝑛 } ) )
37 36 cbvmptv ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑟 ) ∣ Σ 𝑡𝑟 ( 𝑒𝑡 ) = 𝑛 } ) ) = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑒𝑡 ) = 𝑛 } ) )
38 28 37 eqtri ( 𝑟 ∈ 𝒫 𝑇 ↦ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m 𝑟 ) ∣ Σ 𝑢𝑟 ( 𝑑𝑢 ) = 𝑚 } ) ) = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑒𝑡 ) = 𝑛 } ) )
39 fveq1 ( 𝑐 = 𝑒 → ( 𝑐𝑡 ) = ( 𝑒𝑡 ) )
40 39 sumeq2sdv ( 𝑐 = 𝑒 → Σ 𝑡𝑇 ( 𝑐𝑡 ) = Σ 𝑡𝑇 ( 𝑒𝑡 ) )
41 40 eqeq1d ( 𝑐 = 𝑒 → ( Σ 𝑡𝑇 ( 𝑐𝑡 ) = 𝑛 ↔ Σ 𝑡𝑇 ( 𝑒𝑡 ) = 𝑛 ) )
42 41 cbvrabv { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡𝑇 ( 𝑐𝑡 ) = 𝑛 } = { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡𝑇 ( 𝑒𝑡 ) = 𝑛 }
43 42 mpteq2i ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡𝑇 ( 𝑐𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑇 ) ∣ Σ 𝑡𝑇 ( 𝑒𝑡 ) = 𝑛 } )
44 8 43 eqtri 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 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𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )