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	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnprod.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	dvnprod.t	$⊢ φ \to T \in Fin$
	dvnprod.h	$⊢ (φ \land t \in T) \to H (t) : X ⟶ ℂ$
	dvnprod.n	$⊢ φ \to N \in ℕ_{0}$
	dvnprod.dvnh	$⊢ (φ \land t \in T \land k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ$
	dvnprod.f	$⊢ F = (x \in X ⟼ \prod_{t \in T} H (t) (x))$
	dvnprod.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} c (t) = n\})$
Assertion	dvnprod	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x))$

Proof

Step	Hyp	Ref	Expression
1		dvnprod.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvnprod.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		dvnprod.t	$⊢ φ \to T \in Fin$
4		dvnprod.h	$⊢ (φ \land t \in T) \to H (t) : X ⟶ ℂ$
5		dvnprod.n	$⊢ φ \to N \in ℕ_{0}$
6		dvnprod.dvnh	$⊢ (φ \land t \in T \land k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ$
7		dvnprod.f	$⊢ F = (x \in X ⟼ \prod_{t \in T} H (t) (x))$
8		dvnprod.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} c (t) = n\})$
9		fveq2	$⊢ u = t \to d (u) = d (t)$
10	9	cbvsumv	$⊢ \sum_{u \in r} d (u) = \sum_{t \in r} d (t)$
11	10	eqeq1i	$⊢ \sum_{u \in r} d (u) = m \leftrightarrow \sum_{t \in r} d (t) = m$
12	11	rabbii	$⊢ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\} = \{d \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} d (t) = m\}$
13		fveq1	$⊢ d = e \to d (t) = e (t)$
14	13	sumeq2sdv	$⊢ d = e \to \sum_{t \in r} d (t) = \sum_{t \in r} e (t)$
15	14	eqeq1d	$⊢ d = e \to (\sum_{t \in r} d (t) = m \leftrightarrow \sum_{t \in r} e (t) = m)$
16	15	cbvrabv	$⊢ \{d \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} d (t) = m\} = \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\}$
17	12 16	eqtri	$⊢ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\} = \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\}$
18	17	mpteq2i	$⊢ (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\}) = (m \in ℕ_{0} ⟼ \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\})$
19		eqeq2	$⊢ m = n \to (\sum_{t \in r} e (t) = m \leftrightarrow \sum_{t \in r} e (t) = n)$
20	19	rabbidv	$⊢ m = n \to \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\} = \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = n\}$
21		oveq2	$⊢ m = n \to (0 \dots m) = (0 \dots n)$
22	21	oveq1d	$⊢ m = n \to {(0 \dots m)}^{r} = {(0 \dots n)}^{r}$
23		rabeq	$⊢ {(0 \dots m)}^{r} = {(0 \dots n)}^{r} \to \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = n\} = \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\}$
24	22 23	syl	$⊢ m = n \to \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = n\} = \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\}$
25	20 24	eqtrd	$⊢ m = n \to \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\} = \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\}$
26	25	cbvmptv	$⊢ (m \in ℕ_{0} ⟼ \{e \in ({(0 \dots m)}^{r}) \| \sum_{t \in r} e (t) = m\}) = (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\})$
27	18 26	eqtri	$⊢ (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\}) = (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\})$
28	27	mpteq2i	$⊢ (r \in 𝒫 T ⟼ (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\})) = (r \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\}))$
29		sumeq1	$⊢ r = s \to \sum_{t \in r} e (t) = \sum_{t \in s} e (t)$
30	29	eqeq1d	$⊢ r = s \to (\sum_{t \in r} e (t) = n \leftrightarrow \sum_{t \in s} e (t) = n)$
31	30	rabbidv	$⊢ r = s \to \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\} = \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in s} e (t) = n\}$
32		oveq2	$⊢ r = s \to {(0 \dots n)}^{r} = {(0 \dots n)}^{s}$
33		rabeq	$⊢ {(0 \dots n)}^{r} = {(0 \dots n)}^{s} \to \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in s} e (t) = n\} = \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\}$
34	32 33	syl	$⊢ r = s \to \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in s} e (t) = n\} = \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\}$
35	31 34	eqtrd	$⊢ r = s \to \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\} = \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\}$
36	35	mpteq2dv	$⊢ r = s \to (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\}) = (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\})$
37	36	cbvmptv	$⊢ (r \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{r}) \| \sum_{t \in r} e (t) = n\})) = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\}))$
38	28 37	eqtri	$⊢ (r \in 𝒫 T ⟼ (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{r}) \| \sum_{u \in r} d (u) = m\})) = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} e (t) = n\}))$
39		fveq1	$⊢ c = e \to c (t) = e (t)$
40	39	sumeq2sdv	$⊢ c = e \to \sum_{t \in T} c (t) = \sum_{t \in T} e (t)$
41	40	eqeq1d	$⊢ c = e \to (\sum_{t \in T} c (t) = n \leftrightarrow \sum_{t \in T} e (t) = n)$
42	41	cbvrabv	$⊢ \{c \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} c (t) = n\} = \{e \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} e (t) = n\}$
43	42	mpteq2i	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} c (t) = n\}) = (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} e (t) = n\})$
44	8 43	eqtri	$⊢ C = (n \in ℕ_{0} ⟼ \{e \in ({(0 \dots n)}^{T}) \| \sum_{t \in T} e (t) = n\})$
45	1 2 3 4 5 6 7 38 44	dvnprodlem3	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{e \in C (N)} (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x))$
46		fveq1	$⊢ e = c \to e (t) = c (t)$
47	46	fveq2d	$⊢ e = c \to e (t)! = c (t)!$
48	47	prodeq2ad	$⊢ e = c \to \prod_{t \in T} e (t)! = \prod_{t \in T} c (t)!$
49	48	oveq2d	$⊢ e = c \to \frac{N!}{\prod_{t \in T} e (t)!} = \frac{N!}{\prod_{t \in T} c (t)!}$
50	46	fveq2d	$⊢ e = c \to (S D^{n} H (t)) (e (t)) = (S D^{n} H (t)) (c (t))$
51	50	fveq1d	$⊢ e = c \to (S D^{n} H (t)) (e (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
52	51	prodeq2ad	$⊢ e = c \to \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x) = \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x)$
53	49 52	oveq12d	$⊢ e = c \to (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x) = (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x)$
54	53	cbvsumv	$⊢ \sum_{e \in C (N)} (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x) = \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x)$
55		eqid	$⊢ \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x) = \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x)$
56	54 55	eqtri	$⊢ \sum_{e \in C (N)} (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x) = \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x)$
57	56	mpteq2i	$⊢ (x \in X ⟼ \sum_{e \in C (N)} (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x)) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x))$
58	57	a1i	$⊢ φ \to (x \in X ⟼ \sum_{e \in C (N)} (\frac{N!}{\prod_{t \in T} e (t)!}) \prod_{t \in T} (S D^{n} H (t)) (e (t)) (x)) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x))$
59	45 58	eqtrd	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{c \in C (N)} (\frac{N!}{\prod_{t \in T} c (t)!}) \prod_{t \in T} (S D^{n} H (t)) (c (t)) (x))$

Metamath Proof Explorer

Theorem dvnprod

Proof