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

Proof