dvnprodlem2

	Ref	Expression
Hypotheses	dvnprodlem2.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnprodlem2.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	dvnprodlem2.t	$⊢ φ \to T \in Fin$
	dvnprodlem2.h	$⊢ (φ \land t \in T) \to H (t) : X ⟶ ℂ$
	dvnprodlem2.n	$⊢ φ \to N \in ℕ_{0}$
	dvnprodlem2.dvnh	$⊢ (φ \land t \in T \land j \in (0 \dots N)) \to (S D^{n} H (t)) (j) : X ⟶ ℂ$
	dvnprodlem2.c	$⊢ C = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}))$
	dvnprodlem2.r	$⊢ φ \to R \subseteq T$
	dvnprodlem2.z	$⊢ φ \to Z \in (T ∖ R)$
	dvnprodlem2.ind	$⊢ φ \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 C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
	dvnprodlem2.j	$⊢ φ \to J \in (0 \dots N)$
	dvnprodlem2.d	$⊢ D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
Assertion	dvnprodlem2	$⊢ φ \to (S D^{n} (x \in X ⟼ \prod_{t \in R \cup \{Z\}} H (t) (x))) (J) = (x \in X ⟼ \sum_{c \in C (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))$

Proof

Step	Hyp	Ref	Expression
1		dvnprodlem2.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvnprodlem2.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		dvnprodlem2.t	$⊢ φ \to T \in Fin$
4		dvnprodlem2.h	$⊢ (φ \land t \in T) \to H (t) : X ⟶ ℂ$
5		dvnprodlem2.n	$⊢ φ \to N \in ℕ_{0}$
6		dvnprodlem2.dvnh	$⊢ (φ \land t \in T \land j \in (0 \dots N)) \to (S D^{n} H (t)) (j) : X ⟶ ℂ$
7		dvnprodlem2.c	$⊢ C = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}))$
8		dvnprodlem2.r	$⊢ φ \to R \subseteq T$
9		dvnprodlem2.z	$⊢ φ \to Z \in (T ∖ R)$
10		dvnprodlem2.ind	$⊢ φ \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 C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
11		dvnprodlem2.j	$⊢ φ \to J \in (0 \dots N)$
12		dvnprodlem2.d	$⊢ D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
13		nfv	$⊢ Ⅎ t (φ \land x \in X)$
14		nfcv	$⊢ \underline{Ⅎ} t H (Z) (x)$
15		ssfi	$⊢ (T \in Fin \land R \subseteq T) \to R \in Fin$
16	3 8 15	syl2anc	$⊢ φ \to R \in Fin$
17	16	adantr	$⊢ (φ \land x \in X) \to R \in Fin$
18	9	adantr	$⊢ (φ \land x \in X) \to Z \in (T ∖ R)$
19	9	eldifbd	$⊢ φ \to \neg Z \in R$
20	19	adantr	$⊢ (φ \land x \in X) \to \neg Z \in R$
21		simpl	$⊢ (φ \land t \in R) \to φ$
22	8	sselda	$⊢ (φ \land t \in R) \to t \in T$
23	21 22 4	syl2anc	$⊢ (φ \land t \in R) \to H (t) : X ⟶ ℂ$
24	23	adantlr	$⊢ ((φ \land x \in X) \land t \in R) \to H (t) : X ⟶ ℂ$
25		simplr	$⊢ ((φ \land x \in X) \land t \in R) \to x \in X$
26	24 25	ffvelrnd	$⊢ ((φ \land x \in X) \land t \in R) \to H (t) (x) \in ℂ$
27		fveq2	$⊢ t = Z \to H (t) = H (Z)$
28	27	fveq1d	$⊢ t = Z \to H (t) (x) = H (Z) (x)$
29		id	$⊢ φ \to φ$
30		eldifi	$⊢ Z \in (T ∖ R) \to Z \in T$
31	9 30	syl	$⊢ φ \to Z \in T$
32		simpr	$⊢ (φ \land Z \in T) \to Z \in T$
33		id	$⊢ (φ \land Z \in T) \to (φ \land Z \in T)$
34		eleq1	$⊢ t = Z \to (t \in T \leftrightarrow Z \in T)$
35	34	anbi2d	$⊢ t = Z \to ((φ \land t \in T) \leftrightarrow (φ \land Z \in T))$
36	27	feq1d	$⊢ t = Z \to (H (t) : X ⟶ ℂ \leftrightarrow H (Z) : X ⟶ ℂ)$
37	35 36	imbi12d	$⊢ t = Z \to (((φ \land t \in T) \to H (t) : X ⟶ ℂ) \leftrightarrow ((φ \land Z \in T) \to H (Z) : X ⟶ ℂ))$
38	37 4	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T) \to H (Z) : X ⟶ ℂ)$
39	32 33 38	sylc	$⊢ (φ \land Z \in T) \to H (Z) : X ⟶ ℂ$
40	29 31 39	syl2anc	$⊢ φ \to H (Z) : X ⟶ ℂ$
41	40	adantr	$⊢ (φ \land x \in X) \to H (Z) : X ⟶ ℂ$
42		simpr	$⊢ (φ \land x \in X) \to x \in X$
43	41 42	ffvelrnd	$⊢ (φ \land x \in X) \to H (Z) (x) \in ℂ$
44	13 14 17 18 20 26 28 43	fprodsplitsn	$⊢ (φ \land x \in X) \to \prod_{t \in R \cup \{Z\}} H (t) (x) = \prod_{t \in R} H (t) (x) H (Z) (x)$
45	44	mpteq2dva	$⊢ φ \to (x \in X ⟼ \prod_{t \in R \cup \{Z\}} H (t) (x)) = (x \in X ⟼ \prod_{t \in R} H (t) (x) H (Z) (x))$
46	45	oveq2d	$⊢ φ \to S D^{n} (x \in X ⟼ \prod_{t \in R \cup \{Z\}} H (t) (x)) = S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x) H (Z) (x))$
47	46	fveq1d	$⊢ φ \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} H (t) (x) H (Z) (x))) (J)$
48	13 17 26	fprodclf	$⊢ (φ \land x \in X) \to \prod_{t \in R} H (t) (x) \in ℂ$
49		elfznn0	$⊢ J \in (0 \dots N) \to J \in ℕ_{0}$
50	11 49	syl	$⊢ φ \to J \in ℕ_{0}$
51		eqid	$⊢ (x \in X ⟼ \prod_{t \in R} H (t) (x)) = (x \in X ⟼ \prod_{t \in R} H (t) (x))$
52		eqid	$⊢ (x \in X ⟼ H (Z) (x)) = (x \in X ⟼ H (Z) (x))$
53		oveq2	$⊢ s = R \to {(0 \dots n)}^{s} = {(0 \dots n)}^{R}$
54		rabeq	$⊢ {(0 \dots n)}^{s} = {(0 \dots n)}^{R} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\}$
55	53 54	syl	$⊢ s = R \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\}$
56		sumeq1	$⊢ s = R \to \sum_{t \in s} c (t) = \sum_{t \in R} c (t)$
57	56	eqeq1d	$⊢ s = R \to (\sum_{t \in s} c (t) = n \leftrightarrow \sum_{t \in R} c (t) = n)$
58	57	rabbidv	$⊢ s = R \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}$
59	55 58	eqtrd	$⊢ s = R \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}$
60	59	mpteq2dv	$⊢ s = R \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)}^{R}) \| \sum_{t \in R} c (t) = n\})$
61		ssexg	$⊢ (R \subseteq T \land T \in Fin) \to R \in V$
62	8 3 61	syl2anc	$⊢ φ \to R \in V$
63		elpwg	$⊢ R \in V \to (R \in 𝒫 T \leftrightarrow R \subseteq T)$
64	62 63	syl	$⊢ φ \to (R \in 𝒫 T \leftrightarrow R \subseteq T)$
65	8 64	mpbird	$⊢ φ \to R \in 𝒫 T$
66	65	adantr	$⊢ (φ \land k \in (0 \dots J)) \to R \in 𝒫 T$
67		nn0ex	$⊢ ℕ_{0} \in V$
68	67	mptex	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) \in V$
69	68	a1i	$⊢ (φ \land k \in (0 \dots J)) \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) \in V$
70	7 60 66 69	fvmptd3	$⊢ (φ \land k \in (0 \dots J)) \to C (R) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\})$
71		oveq2	$⊢ n = k \to (0 \dots n) = (0 \dots k)$
72	71	oveq1d	$⊢ n = k \to {(0 \dots n)}^{R} = {(0 \dots k)}^{R}$
73		rabeq	$⊢ {(0 \dots n)}^{R} = {(0 \dots k)}^{R} \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\}$
74	72 73	syl	$⊢ n = k \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\}$
75		eqeq2	$⊢ n = k \to (\sum_{t \in R} c (t) = n \leftrightarrow \sum_{t \in R} c (t) = k)$
76	75	rabbidv	$⊢ n = k \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
77	74 76	eqtrd	$⊢ n = k \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
78	77	adantl	$⊢ ((φ \land k \in (0 \dots J)) \land n = k) \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
79		elfznn0	$⊢ k \in (0 \dots J) \to k \in ℕ_{0}$
80	79	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℕ_{0}$
81		fzfid	$⊢ φ \to (0 \dots k) \in Fin$
82		mapfi	$⊢ ((0 \dots k) \in Fin \land R \in Fin) \to {(0 \dots k)}^{R} \in Fin$
83	81 16 82	syl2anc	$⊢ φ \to {(0 \dots k)}^{R} \in Fin$
84	83	adantr	$⊢ (φ \land k \in (0 \dots J)) \to {(0 \dots k)}^{R} \in Fin$
85		ssrab2	$⊢ \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \subseteq {(0 \dots k)}^{R}$
86	85	a1i	$⊢ (φ \land k \in (0 \dots J)) \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \subseteq {(0 \dots k)}^{R}$
87	84 86	ssexd	$⊢ (φ \land k \in (0 \dots J)) \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in V$
88	70 78 80 87	fvmptd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
89		ssfi	$⊢ ({(0 \dots k)}^{R} \in Fin \land \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \subseteq {(0 \dots k)}^{R}) \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in Fin$
90	83 85 89	sylancl	$⊢ φ \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in Fin$
91	90	adantr	$⊢ (φ \land k \in (0 \dots J)) \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in Fin$
92	88 91	eqeltrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \in Fin$
93	92	adantr	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \to C (R) (k) \in Fin$
94	79	faccld	$⊢ k \in (0 \dots J) \to k! \in ℕ$
95	94	nncnd	$⊢ k \in (0 \dots J) \to k! \in ℂ$
96	95	ad2antlr	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to k! \in ℂ$
97	16	adantr	$⊢ (φ \land c \in C (R) (k)) \to R \in Fin$
98	97	adantlr	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to R \in Fin$
99		elfznn0	$⊢ z \in (0 \dots k) \to z \in ℕ_{0}$
100	99	ssriv	$⊢ (0 \dots k) \subseteq ℕ_{0}$
101	100	a1i	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to (0 \dots k) \subseteq ℕ_{0}$
102		simpr	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to c \in C (R) (k)$
103	88	eleq2d	$⊢ (φ \land k \in (0 \dots J)) \to (c \in C (R) (k) \leftrightarrow c \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\})$
104	103	adantr	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to (c \in C (R) (k) \leftrightarrow c \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\})$
105	102 104	mpbid	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to c \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
106	85	sseli	$⊢ c \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \to c \in ({(0 \dots k)}^{R})$
107	105 106	syl	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to c \in ({(0 \dots k)}^{R})$
108		elmapi	$⊢ c \in ({(0 \dots k)}^{R}) \to c : R ⟶ (0 \dots k)$
109	107 108	syl	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to c : R ⟶ (0 \dots k)$
110	109	adantr	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c : R ⟶ (0 \dots k)$
111		simpr	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to t \in R$
112	110 111	ffvelrnd	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t) \in (0 \dots k)$
113	101 112	sseldd	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t) \in ℕ_{0}$
114	113	faccld	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t)! \in ℕ$
115	114	nncnd	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t)! \in ℂ$
116	98 115	fprodcl	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to \prod_{t \in R} c (t)! \in ℂ$
117	114	nnne0d	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t)! \neq 0$
118	98 115 117	fprodn0	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to \prod_{t \in R} c (t)! \neq 0$
119	96 116 118	divcld	$⊢ ((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \to \frac{k!}{\prod_{t \in R} c (t)!} \in ℂ$
120	119	adantlr	$⊢ (((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \to \frac{k!}{\prod_{t \in R} c (t)!} \in ℂ$
121	98	adantlr	$⊢ (((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \to R \in Fin$
122	29	ad4antr	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to φ$
123	122 22	sylancom	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to t \in T$
124		elfzuz3	$⊢ k \in (0 \dots J) \to J \in ℤ_{\geq k}$
125		fzss2	$⊢ J \in ℤ_{\geq k} \to (0 \dots k) \subseteq (0 \dots J)$
126	124 125	syl	$⊢ k \in (0 \dots J) \to (0 \dots k) \subseteq (0 \dots J)$
127	126	adantl	$⊢ (φ \land k \in (0 \dots J)) \to (0 \dots k) \subseteq (0 \dots J)$
128	50	nn0zd	$⊢ φ \to J \in ℤ$
129	5	nn0zd	$⊢ φ \to N \in ℤ$
130		elfzle2	$⊢ J \in (0 \dots N) \to J \leq N$
131	11 130	syl	$⊢ φ \to J \leq N$
132	128 129 131	3jca	$⊢ φ \to (J \in ℤ \land N \in ℤ \land J \leq N)$
133		eluz2	$⊢ N \in ℤ_{\geq J} \leftrightarrow (J \in ℤ \land N \in ℤ \land J \leq N)$
134	132 133	sylibr	$⊢ φ \to N \in ℤ_{\geq J}$
135		fzss2	$⊢ N \in ℤ_{\geq J} \to (0 \dots J) \subseteq (0 \dots N)$
136	134 135	syl	$⊢ φ \to (0 \dots J) \subseteq (0 \dots N)$
137	136	adantr	$⊢ (φ \land k \in (0 \dots J)) \to (0 \dots J) \subseteq (0 \dots N)$
138	127 137	sstrd	$⊢ (φ \land k \in (0 \dots J)) \to (0 \dots k) \subseteq (0 \dots N)$
139	138	ad2antrr	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to (0 \dots k) \subseteq (0 \dots N)$
140	139 112	sseldd	$⊢ (((φ \land k \in (0 \dots J)) \land c \in C (R) (k)) \land t \in R) \to c (t) \in (0 \dots N)$
141	140	adantllr	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to c (t) \in (0 \dots N)$
142		fvex	$⊢ c (t) \in V$
143		eleq1	$⊢ j = c (t) \to (j \in (0 \dots N) \leftrightarrow c (t) \in (0 \dots N))$
144	143	3anbi3d	$⊢ j = c (t) \to ((φ \land t \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land t \in T \land c (t) \in (0 \dots N)))$
145		fveq2	$⊢ j = c (t) \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (c (t))$
146	145	feq1d	$⊢ j = c (t) \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (t)) (c (t)) : X ⟶ ℂ)$
147	144 146	imbi12d	$⊢ j = c (t) \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 c (t) \in (0 \dots N)) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ))$
148	142 147 6	vtocl	$⊢ (φ \land t \in T \land c (t) \in (0 \dots N)) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
149	122 123 141 148	syl3anc	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
150		simpllr	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to x \in X$
151	149 150	ffvelrnd	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \land t \in R) \to (S D^{n} H (t)) (c (t)) (x) \in ℂ$
152	121 151	fprodcl	$⊢ (((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \to \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
153	120 152	mulcld	$⊢ (((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
154	93 153	fsumcl	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \to \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
155	154	fmpttd	$⊢ (φ \land k \in (0 \dots J)) \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) : X ⟶ ℂ$
156	10	adantr	$⊢ (φ \land k \in (0 \dots J)) \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 C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
157		0zd	$⊢ (φ \land k \in (0 \dots J)) \to 0 \in ℤ$
158	129	adantr	$⊢ (φ \land k \in (0 \dots J)) \to N \in ℤ$
159		elfzelz	$⊢ k \in (0 \dots J) \to k \in ℤ$
160	159	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℤ$
161		elfzle1	$⊢ k \in (0 \dots J) \to 0 \leq k$
162	161	adantl	$⊢ (φ \land k \in (0 \dots J)) \to 0 \leq k$
163	160	zred	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℝ$
164	50	nn0red	$⊢ φ \to J \in ℝ$
165	164	adantr	$⊢ (φ \land k \in (0 \dots J)) \to J \in ℝ$
166	158	zred	$⊢ (φ \land k \in (0 \dots J)) \to N \in ℝ$
167		elfzle2	$⊢ k \in (0 \dots J) \to k \leq J$
168	167	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \leq J$
169	131	adantr	$⊢ (φ \land k \in (0 \dots J)) \to J \leq N$
170	163 165 166 168 169	letrd	$⊢ (φ \land k \in (0 \dots J)) \to k \leq N$
171	157 158 160 162 170	elfzd	$⊢ (φ \land k \in (0 \dots J)) \to k \in (0 \dots N)$
172		rspa	$⊢ (\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 C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) \land k \in (0 \dots N)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
173	156 171 172	syl2anc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
174	173	feq1d	$⊢ (φ \land k \in (0 \dots J)) \to ((S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) : X ⟶ ℂ \leftrightarrow (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) : X ⟶ ℂ)$
175	155 174	mpbird	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) : X ⟶ ℂ$
176	31	adantr	$⊢ (φ \land k \in (0 \dots J)) \to Z \in T$
177		simpl	$⊢ (φ \land k \in (0 \dots J)) \to φ$
178	177 176 171	3jca	$⊢ (φ \land k \in (0 \dots J)) \to (φ \land Z \in T \land k \in (0 \dots N))$
179	34	3anbi2d	$⊢ t = Z \to ((φ \land t \in T \land k \in (0 \dots N)) \leftrightarrow (φ \land Z \in T \land k \in (0 \dots N)))$
180	27	oveq2d	$⊢ t = Z \to S D^{n} H (t) = S D^{n} H (Z)$
181	180	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (k) = (S D^{n} H (Z)) (k)$
182	181	feq1d	$⊢ t = Z \to ((S D^{n} H (t)) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (k) : X ⟶ ℂ)$
183	179 182	imbi12d	$⊢ t = Z \to (((φ \land t \in T \land k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ) \leftrightarrow ((φ \land Z \in T \land k \in (0 \dots N)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ))$
184		eleq1	$⊢ j = k \to (j \in (0 \dots N) \leftrightarrow k \in (0 \dots N))$
185	184	3anbi3d	$⊢ j = k \to ((φ \land t \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land t \in T \land k \in (0 \dots N)))$
186		fveq2	$⊢ j = k \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (k)$
187	186	feq1d	$⊢ j = k \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (t)) (k) : X ⟶ ℂ)$
188	185 187	imbi12d	$⊢ j = k \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 k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ))$
189	188 6	chvarvv	$⊢ (φ \land t \in T \land k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ$
190	183 189	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T \land k \in (0 \dots N)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ)$
191	176 178 190	sylc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ$
192	40	feqmptd	$⊢ φ \to H (Z) = (x \in X ⟼ H (Z) (x))$
193	192	eqcomd	$⊢ φ \to (x \in X ⟼ H (Z) (x)) = H (Z)$
194	193	oveq2d	$⊢ φ \to S D^{n} (x \in X ⟼ H (Z) (x)) = S D^{n} H (Z)$
195	194	fveq1d	$⊢ φ \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) = (S D^{n} H (Z)) (k)$
196	195	adantr	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) = (S D^{n} H (Z)) (k)$
197	196	feq1d	$⊢ (φ \land k \in (0 \dots J)) \to ((S D^{n} (x \in X ⟼ H (Z) (x))) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (k) : X ⟶ ℂ)$
198	191 197	mpbird	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) : X ⟶ ℂ$
199		fveq2	$⊢ y = x \to H (t) (y) = H (t) (x)$
200	199	prodeq2ad	$⊢ y = x \to \prod_{t \in R} H (t) (y) = \prod_{t \in R} H (t) (x)$
201	200	cbvmptv	$⊢ (y \in X ⟼ \prod_{t \in R} H (t) (y)) = (x \in X ⟼ \prod_{t \in R} H (t) (x))$
202	201	oveq2i	$⊢ S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y)) = S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))$
203	202	fveq1i	$⊢ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k) = (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k)$
204	203	mpteq2i	$⊢ (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) = (k \in (0 \dots J) ⟼ (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k))$
205		fveq2	$⊢ y = x \to H (Z) (y) = H (Z) (x)$
206	205	cbvmptv	$⊢ (y \in X ⟼ H (Z) (y)) = (x \in X ⟼ H (Z) (x))$
207	206	oveq2i	$⊢ S D^{n} (y \in X ⟼ H (Z) (y)) = S D^{n} (x \in X ⟼ H (Z) (x))$
208	207	fveq1i	$⊢ (S D^{n} (y \in X ⟼ H (Z) (y))) (k) = (S D^{n} (x \in X ⟼ H (Z) (x))) (k)$
209	208	mpteq2i	$⊢ (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) = (k \in (0 \dots J) ⟼ (S D^{n} (x \in X ⟼ H (Z) (x))) (k))$
210	1 2 48 43 50 51 52 175 198 204 209	dvnmul	$⊢ φ \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x) H (Z) (x))) (J) = (x \in X ⟼ \sum_{k = 0}^{J} (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x))$
211	203	a1i	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k) = (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k)$
212	10	r19.21bi	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
213	177 171 212	syl2anc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
214	211 213	eqtrd	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
215	214	mpteq2dva	$⊢ φ \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) = (k \in (0 \dots J) ⟼ (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)))$
216		mptexg	$⊢ X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) \in V$
217	2 216	syl	$⊢ φ \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) \in V$
218	217	adantr	$⊢ (φ \land k \in (0 \dots J)) \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) \in V$
219	215 218	fvmpt2d	$⊢ (φ \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
220	219	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
221	220	fveq1d	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) = (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) (x)$
222	42	adantr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to x \in X$
223	154	an32s	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
224		eqid	$⊢ (x \in X ⟼ \sum_{c \in C (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 C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x))$
225	224	fvmpt2	$⊢ (x \in X \land \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ) \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) (x) = \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
226	222 223 225	syl2anc	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (x \in X ⟼ \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)) (x) = \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
227	221 226	eqtrd	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) = \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
228		fveq2	$⊢ k = j \to (S D^{n} (y \in X ⟼ H (Z) (y))) (k) = (S D^{n} (y \in X ⟼ H (Z) (y))) (j)$
229	228	cbvmptv	$⊢ (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) = (j \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (j))$
230	229	a1i	$⊢ φ \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) = (j \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (j))$
231	207 194	syl5eq	$⊢ φ \to S D^{n} (y \in X ⟼ H (Z) (y)) = S D^{n} H (Z)$
232	231	fveq1d	$⊢ φ \to (S D^{n} (y \in X ⟼ H (Z) (y))) (j) = (S D^{n} H (Z)) (j)$
233	232	mpteq2dv	$⊢ φ \to (j \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (j)) = (j \in (0 \dots J) ⟼ (S D^{n} H (Z)) (j))$
234	230 233	eqtrd	$⊢ φ \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) = (j \in (0 \dots J) ⟼ (S D^{n} H (Z)) (j))$
235	234	adantr	$⊢ (φ \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) = (j \in (0 \dots J) ⟼ (S D^{n} H (Z)) (j))$
236		fveq2	$⊢ j = J - k \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - k)$
237	236	adantl	$⊢ ((φ \land k \in (0 \dots J)) \land j = J - k) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - k)$
238		0zd	$⊢ k \in (0 \dots J) \to 0 \in ℤ$
239		elfzel2	$⊢ k \in (0 \dots J) \to J \in ℤ$
240	239 159	zsubcld	$⊢ k \in (0 \dots J) \to J - k \in ℤ$
241	238 239 240	3jca	$⊢ k \in (0 \dots J) \to (0 \in ℤ \land J \in ℤ \land J - k \in ℤ)$
242	239	zred	$⊢ k \in (0 \dots J) \to J \in ℝ$
243	79	nn0red	$⊢ k \in (0 \dots J) \to k \in ℝ$
244	242 243	subge0d	$⊢ k \in (0 \dots J) \to (0 \leq J - k \leftrightarrow k \leq J)$
245	167 244	mpbird	$⊢ k \in (0 \dots J) \to 0 \leq J - k$
246	242 243	subge02d	$⊢ k \in (0 \dots J) \to (0 \leq k \leftrightarrow J - k \leq J)$
247	161 246	mpbid	$⊢ k \in (0 \dots J) \to J - k \leq J$
248	241 245 247	jca32	$⊢ k \in (0 \dots J) \to ((0 \in ℤ \land J \in ℤ \land J - k \in ℤ) \land (0 \leq J - k \land J - k \leq J))$
249	248	adantl	$⊢ (φ \land k \in (0 \dots J)) \to ((0 \in ℤ \land J \in ℤ \land J - k \in ℤ) \land (0 \leq J - k \land J - k \leq J))$
250		elfz2	$⊢ J - k \in (0 \dots J) \leftrightarrow ((0 \in ℤ \land J \in ℤ \land J - k \in ℤ) \land (0 \leq J - k \land J - k \leq J))$
251	249 250	sylibr	$⊢ (φ \land k \in (0 \dots J)) \to J - k \in (0 \dots J)$
252		fvex	$⊢ (S D^{n} H (Z)) (J - k) \in V$
253	252	a1i	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) \in V$
254	235 237 251 253	fvmptd	$⊢ (φ \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) = (S D^{n} H (Z)) (J - k)$
255	254	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) = (S D^{n} H (Z)) (J - k)$
256	255	fveq1d	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = (S D^{n} H (Z)) (J - k) (x)$
257	227 256	oveq12d	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
258	257	oveq2d	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = (\binom{J}{k}) \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
259	92	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to C (R) (k) \in Fin$
260		ovex	$⊢ J - k \in V$
261		eleq1	$⊢ j = J - k \to (j \in (0 \dots J) \leftrightarrow J - k \in (0 \dots J))$
262	261	anbi2d	$⊢ j = J - k \to ((φ \land j \in (0 \dots J)) \leftrightarrow (φ \land J - k \in (0 \dots J)))$
263	236	feq1d	$⊢ j = J - k \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (J - k) : X ⟶ ℂ)$
264	262 263	imbi12d	$⊢ j = J - k \to (((φ \land j \in (0 \dots J)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land J - k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ))$
265		eleq1	$⊢ k = j \to (k \in (0 \dots J) \leftrightarrow j \in (0 \dots J))$
266	265	anbi2d	$⊢ k = j \to ((φ \land k \in (0 \dots J)) \leftrightarrow (φ \land j \in (0 \dots J)))$
267		fveq2	$⊢ k = j \to (S D^{n} H (Z)) (k) = (S D^{n} H (Z)) (j)$
268	267	feq1d	$⊢ k = j \to ((S D^{n} H (Z)) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
269	266 268	imbi12d	$⊢ k = j \to (((φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ) \leftrightarrow ((φ \land j \in (0 \dots J)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ))$
270	269 191	chvarvv	$⊢ (φ \land j \in (0 \dots J)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ$
271	260 264 270	vtocl	$⊢ (φ \land J - k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
272	177 251 271	syl2anc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
273	272	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
274	273 222	ffvelrnd	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) (x) \in ℂ$
275		anass	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \leftrightarrow (φ \land (k \in (0 \dots J) \land x \in X))$
276		ancom	$⊢ (k \in (0 \dots J) \land x \in X) \leftrightarrow (x \in X \land k \in (0 \dots J))$
277	276	anbi2i	$⊢ (φ \land (k \in (0 \dots J) \land x \in X)) \leftrightarrow (φ \land (x \in X \land k \in (0 \dots J)))$
278		anass	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \leftrightarrow (φ \land (x \in X \land k \in (0 \dots J)))$
279	278	bicomi	$⊢ (φ \land (x \in X \land k \in (0 \dots J))) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
280	277 279	bitri	$⊢ (φ \land (k \in (0 \dots J) \land x \in X)) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
281	275 280	bitri	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
282	281	anbi1i	$⊢ (((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \leftrightarrow (((φ \land x \in X) \land k \in (0 \dots J)) \land c \in C (R) (k))$
283	282	imbi1i	$⊢ ((((φ \land k \in (0 \dots J)) \land x \in X) \land c \in C (R) (k)) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ) \leftrightarrow ((((φ \land x \in X) \land k \in (0 \dots J)) \land c \in C (R) (k)) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ)$
284	153 283	mpbi	$⊢ (((φ \land x \in X) \land k \in (0 \dots J)) \land c \in C (R) (k)) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
285	259 274 284	fsummulc1	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) = \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
286	285	oveq2d	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) = (\binom{J}{k}) \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
287	177 50	syl	$⊢ (φ \land k \in (0 \dots J)) \to J \in ℕ_{0}$
288	287 160	bccld	$⊢ (φ \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℕ_{0}$
289	288	nn0cnd	$⊢ (φ \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℂ$
290	289	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℂ$
291	274	adantr	$⊢ (((φ \land x \in X) \land k \in (0 \dots J)) \land c \in C (R) (k)) \to (S D^{n} H (Z)) (J - k) (x) \in ℂ$
292	284 291	mulcld	$⊢ (((φ \land x \in X) \land k \in (0 \dots J)) \land c \in C (R) (k)) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) \in ℂ$
293	259 290 292	fsummulc2	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) \sum_{c \in C (R) (k)} (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) = \sum_{c \in C (R) (k)} (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
294	258 286 293	3eqtrd	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = \sum_{c \in C (R) (k)} (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
295	294	sumeq2dv	$⊢ (φ \land x \in X) \to \sum_{k = 0}^{J} (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = \sum_{k = 0}^{J} \sum_{c \in C (R) (k)} (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
296		vex	$⊢ k \in V$
297		vex	$⊢ c \in V$
298	296 297	op1std	$⊢ p = ⟨k, c⟩ \to 1^{st} (p) = k$
299	298	oveq2d	$⊢ p = ⟨k, c⟩ \to (\binom{J}{1^{st} (p)}) = (\binom{J}{k})$
300	298	fveq2d	$⊢ p = ⟨k, c⟩ \to 1^{st} (p)! = k!$
301	296 297	op2ndd	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) = c$
302	301	fveq1d	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) (t) = c (t)$
303	302	fveq2d	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) (t)! = c (t)!$
304	303	prodeq2ad	$⊢ p = ⟨k, c⟩ \to \prod_{t \in R} 2^{nd} (p) (t)! = \prod_{t \in R} c (t)!$
305	300 304	oveq12d	$⊢ p = ⟨k, c⟩ \to \frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!} = \frac{k!}{\prod_{t \in R} c (t)!}$
306	302	fveq2d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) = (S D^{n} H (t)) (c (t))$
307	306	fveq1d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
308	307	prodeq2ad	$⊢ p = ⟨k, c⟩ \to \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
309	305 308	oveq12d	$⊢ p = ⟨k, c⟩ \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
310	298	oveq2d	$⊢ p = ⟨k, c⟩ \to J - 1^{st} (p) = J - k$
311	310	fveq2d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) = (S D^{n} H (Z)) (J - k)$
312	311	fveq1d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (S D^{n} H (Z)) (J - k) (x)$
313	309 312	oveq12d	$⊢ p = ⟨k, c⟩ \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
314	299 313	oveq12d	$⊢ p = ⟨k, c⟩ \to (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x)$
315		fzfid	$⊢ (φ \land x \in X) \to (0 \dots J) \in Fin$
316	290	adantrr	$⊢ ((φ \land x \in X) \land (k \in (0 \dots J) \land c \in C (R) (k))) \to (\binom{J}{k}) \in ℂ$
317	292	anasss	$⊢ ((φ \land x \in X) \land (k \in (0 \dots J) \land c \in C (R) (k))) \to (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) \in ℂ$
318	316 317	mulcld	$⊢ ((φ \land x \in X) \land (k \in (0 \dots J) \land c \in C (R) (k))) \to (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) \in ℂ$
319	314 315 259 318	fsum2d	$⊢ (φ \land x \in X) \to \sum_{k = 0}^{J} \sum_{c \in C (R) (k)} (\binom{J}{k}) (\frac{k!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (J - k) (x) = \sum_{p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))} (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x)$
320		ovex	$⊢ J - c (Z) \in V$
321	297	resex	$⊢ {c ↾}_{R} \in V$
322	320 321	op1std	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 1^{st} (p) = J - c (Z)$
323	322	oveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (\binom{J}{1^{st} (p)}) = (\binom{J}{J - c (Z)})$
324	322	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 1^{st} (p)! = (J - c (Z))!$
325	320 321	op2ndd	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) = {c ↾}_{R}$
326	325	fveq1d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) (t) = ({c ↾}_{R}) (t)$
327	326	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) (t)! = ({c ↾}_{R}) (t)!$
328	327	prodeq2ad	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to \prod_{t \in R} 2^{nd} (p) (t)! = \prod_{t \in R} ({c ↾}_{R}) (t)!$
329	324 328	oveq12d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to \frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!} = \frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}$
330	326	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) = (S D^{n} H (t)) (({c ↾}_{R}) (t))$
331	330	fveq1d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x)$
332	331	prodeq2ad	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x)$
333	329 332	oveq12d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x)$
334	322	oveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to J - 1^{st} (p) = J - (J - c (Z))$
335	334	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) = (S D^{n} H (Z)) (J - (J - c (Z)))$
336	335	fveq1d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (S D^{n} H (Z)) (J - (J - c (Z))) (x)$
337	333 336	oveq12d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x)$
338	323 337	oveq12d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (\binom{J}{J - c (Z)}) (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x)$
339		oveq2	$⊢ s = R \cup \{Z\} \to {(0 \dots n)}^{s} = {(0 \dots n)}^{(R \cup \{Z\})}$
340		rabeq	$⊢ {(0 \dots n)}^{s} = {(0 \dots n)}^{(R \cup \{Z\})} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\}$
341	339 340	syl	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\}$
342		sumeq1	$⊢ s = R \cup \{Z\} \to \sum_{t \in s} c (t) = \sum_{t \in R \cup \{Z\}} c (t)$
343	342	eqeq1d	$⊢ s = R \cup \{Z\} \to (\sum_{t \in s} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = n)$
344	343	rabbidv	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
345	341 344	eqtrd	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
346	345	mpteq2dv	$⊢ s = R \cup \{Z\} \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)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\})$
347	31	snssd	$⊢ φ \to \{Z\} \subseteq T$
348	8 347	unssd	$⊢ φ \to R \cup \{Z\} \subseteq T$
349	3 348	ssexd	$⊢ φ \to R \cup \{Z\} \in V$
350		elpwg	$⊢ R \cup \{Z\} \in V \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
351	349 350	syl	$⊢ φ \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
352	348 351	mpbird	$⊢ φ \to R \cup \{Z\} \in 𝒫 T$
353	67	mptex	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
354	353	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
355	7 346 352 354	fvmptd3	$⊢ φ \to C (R \cup \{Z\}) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\})$
356		oveq2	$⊢ n = J \to (0 \dots n) = (0 \dots J)$
357	356	oveq1d	$⊢ n = J \to {(0 \dots n)}^{(R \cup \{Z\})} = {(0 \dots J)}^{(R \cup \{Z\})}$
358		rabeq	$⊢ {(0 \dots n)}^{(R \cup \{Z\})} = {(0 \dots J)}^{(R \cup \{Z\})} \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
359	357 358	syl	$⊢ n = J \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
360		eqeq2	$⊢ n = J \to (\sum_{t \in R \cup \{Z\}} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = J)$
361	360	rabbidv	$⊢ n = J \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
362	359 361	eqtrd	$⊢ n = J \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
363	362	adantl	$⊢ (φ \land n = J) \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
364		ovex	$⊢ {(0 \dots J)}^{(R \cup \{Z\})} \in V$
365	364	rabex	$⊢ \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
366	365	a1i	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
367	355 363 50 366	fvmptd	$⊢ φ \to C (R \cup \{Z\}) (J) = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
368		fzfid	$⊢ φ \to (0 \dots J) \in Fin$
369		snfi	$⊢ \{Z\} \in Fin$
370	369	a1i	$⊢ φ \to \{Z\} \in Fin$
371		unfi	$⊢ (R \in Fin \land \{Z\} \in Fin) \to R \cup \{Z\} \in Fin$
372	16 370 371	syl2anc	$⊢ φ \to R \cup \{Z\} \in Fin$
373		mapfi	$⊢ ((0 \dots J) \in Fin \land R \cup \{Z\} \in Fin) \to {(0 \dots J)}^{(R \cup \{Z\})} \in Fin$
374	368 372 373	syl2anc	$⊢ φ \to {(0 \dots J)}^{(R \cup \{Z\})} \in Fin$
375		ssrab2	$⊢ \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
376	375	a1i	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
377		ssfi	$⊢ ({(0 \dots J)}^{(R \cup \{Z\})} \in Fin \land \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \subseteq {(0 \dots J)}^{(R \cup \{Z\})}) \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in Fin$
378	374 376 377	syl2anc	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in Fin$
379	367 378	eqeltrd	$⊢ φ \to C (R \cup \{Z\}) (J) \in Fin$
380	379	adantr	$⊢ (φ \land x \in X) \to C (R \cup \{Z\}) (J) \in Fin$
381	7 50 12 3 31 19 348	dvnprodlem1	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
382	381	adantr	$⊢ (φ \land x \in X) \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
383		simpr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in C (R \cup \{Z\}) (J)$
384		opex	$⊢ ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
385	384	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
386	12	fvmpt2	$⊢ (c \in C (R \cup \{Z\}) (J) \land ⟨J - c (Z), {c ↾}_{R}⟩ \in V) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
387	383 385 386	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
388	387	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
389	50	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J \in ℕ_{0}$
390		eliun	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
391	390	biimpi	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
392	391	adantl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
393		nfv	$⊢ Ⅎ k φ$
394		nfcv	$⊢ \underline{Ⅎ} k p$
395		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
396	394 395	nfel	$⊢ Ⅎ k p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
397	393 396	nfan	$⊢ Ⅎ k (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
398		nfv	$⊢ Ⅎ k 1^{st} (p) \in (0 \dots J)$
399		xp1st	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in \{k\}$
400		elsni	$⊢ 1^{st} (p) \in \{k\} \to 1^{st} (p) = k$
401	399 400	syl	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) = k$
402	401	adantl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) = k$
403		simpl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in (0 \dots J)$
404	402 403	eqeltrd	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
405	404	ex	$⊢ k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
406	405	a1i	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J)))$
407	397 398 406	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
408	392 407	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
409		elfzelz	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℤ$
410	408 409	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℤ$
411	389 410	bccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℕ_{0}$
412	411	nn0cnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
413	412	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
414		elfznn0	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℕ_{0}$
415	408 414	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℕ_{0}$
416	415	faccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℕ$
417	416	nncnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
418	417	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
419	16	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
420		nfv	$⊢ Ⅎ k 2^{nd} (p) : R ⟶ (0 \dots J)$
421	88 86	eqsstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots k)}^{R}$
422		ovex	$⊢ (0 \dots J) \in V$
423	422	a1i	$⊢ k \in (0 \dots J) \to (0 \dots J) \in V$
424		mapss	$⊢ ((0 \dots J) \in V \land (0 \dots k) \subseteq (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
425	423 126 424	syl2anc	$⊢ k \in (0 \dots J) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
426	425	adantl	$⊢ (φ \land k \in (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
427	421 426	sstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
428	427	3adant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
429		xp2nd	$⊢ p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) \in C (R) (k)$
430	429	3ad2ant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in C (R) (k)$
431	428 430	sseldd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in ({(0 \dots J)}^{R})$
432		elmapi	$⊢ 2^{nd} (p) \in ({(0 \dots J)}^{R}) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
433	431 432	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
434	433	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) : R ⟶ (0 \dots J)))$
435	434	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) : R ⟶ (0 \dots J)))$
436	397 420 435	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) : R ⟶ (0 \dots J))$
437	392 436	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
438	437	ffvelrnda	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in (0 \dots J)$
439		elfznn0	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t) \in ℕ_{0}$
440	439	faccld	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℕ$
441	440	nncnd	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℂ$
442	438 441	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℂ$
443	419 442	fprodcl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \in ℂ$
444	443	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \in ℂ$
445	438 440	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℕ$
446		nnne0	$⊢ 2^{nd} (p) (t)! \in ℕ \to 2^{nd} (p) (t)! \neq 0$
447	445 446	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \neq 0$
448	419 442 447	fprodn0	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \neq 0$
449	448	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \neq 0$
450	418 444 449	divcld	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!} \in ℂ$
451	17	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
452		simpll	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to φ$
453	452 22	sylancom	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to t \in T$
454	452 136	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to (0 \dots J) \subseteq (0 \dots N)$
455	454 438	sseldd	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in (0 \dots N)$
456	452 453 455	3jca	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to (φ \land t \in T \land 2^{nd} (p) (t) \in (0 \dots N))$
457		eleq1	$⊢ j = 2^{nd} (p) (t) \to (j \in (0 \dots N) \leftrightarrow 2^{nd} (p) (t) \in (0 \dots N))$
458	457	3anbi3d	$⊢ j = 2^{nd} (p) (t) \to ((φ \land t \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land t \in T \land 2^{nd} (p) (t) \in (0 \dots N)))$
459		fveq2	$⊢ j = 2^{nd} (p) (t) \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (2^{nd} (p) (t))$
460	459	feq1d	$⊢ j = 2^{nd} (p) (t) \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (t)) (2^{nd} (p) (t)) : X ⟶ ℂ)$
461	458 460	imbi12d	$⊢ j = 2^{nd} (p) (t) \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 2^{nd} (p) (t) \in (0 \dots N)) \to (S D^{n} H (t)) (2^{nd} (p) (t)) : X ⟶ ℂ))$
462	461 6	vtoclg	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to ((φ \land t \in T \land 2^{nd} (p) (t) \in (0 \dots N)) \to (S D^{n} H (t)) (2^{nd} (p) (t)) : X ⟶ ℂ)$
463	438 456 462	sylc	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to (S D^{n} H (t)) (2^{nd} (p) (t)) : X ⟶ ℂ$
464	463	adantllr	$⊢ (((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to (S D^{n} H (t)) (2^{nd} (p) (t)) : X ⟶ ℂ$
465	25	adantlr	$⊢ (((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to x \in X$
466	464 465	ffvelrnd	$⊢ (((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to (S D^{n} H (t)) (2^{nd} (p) (t)) (x) \in ℂ$
467	451 466	fprodcl	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) \in ℂ$
468	450 467	mulcld	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) \in ℂ$
469		nfv	$⊢ Ⅎ k J - 1^{st} (p) \in (0 \dots J)$
470		simp1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to φ$
471	404	3adant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
472		fznn0sub2	$⊢ 1^{st} (p) \in (0 \dots J) \to J - 1^{st} (p) \in (0 \dots J)$
473	472	adantl	$⊢ (φ \land 1^{st} (p) \in (0 \dots J)) \to J - 1^{st} (p) \in (0 \dots J)$
474	470 471 473	syl2anc	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
475	474	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to J - 1^{st} (p) \in (0 \dots J)))$
476	475	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to J - 1^{st} (p) \in (0 \dots J)))$
477	397 469 476	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to J - 1^{st} (p) \in (0 \dots J))$
478	392 477	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
479		simpl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to φ$
480	479 31	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to Z \in T$
481	479 136	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (0 \dots J) \subseteq (0 \dots N)$
482	481 478	sseldd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots N)$
483	479 480 482	3jca	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (φ \land Z \in T \land J - 1^{st} (p) \in (0 \dots N))$
484		eleq1	$⊢ j = J - 1^{st} (p) \to (j \in (0 \dots N) \leftrightarrow J - 1^{st} (p) \in (0 \dots N))$
485	484	3anbi3d	$⊢ j = J - 1^{st} (p) \to ((φ \land Z \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land Z \in T \land J - 1^{st} (p) \in (0 \dots N)))$
486		fveq2	$⊢ j = J - 1^{st} (p) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - 1^{st} (p))$
487	486	feq1d	$⊢ j = J - 1^{st} (p) \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ)$
488	485 487	imbi12d	$⊢ j = J - 1^{st} (p) \to (((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land Z \in T \land J - 1^{st} (p) \in (0 \dots N)) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ))$
489		simp2	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to Z \in T$
490		id	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (φ \land Z \in T \land j \in (0 \dots N))$
491	34	3anbi2d	$⊢ t = Z \to ((φ \land t \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land Z \in T \land j \in (0 \dots N)))$
492	180	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (j) = (S D^{n} H (Z)) (j)$
493	492	feq1d	$⊢ t = Z \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
494	491 493	imbi12d	$⊢ t = Z \to (((φ \land t \in T \land j \in (0 \dots N)) \to (S D^{n} H (t)) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ))$
495	494 6	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
496	489 490 495	sylc	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ$
497	488 496	vtoclg	$⊢ J - 1^{st} (p) \in (0 \dots J) \to ((φ \land Z \in T \land J - 1^{st} (p) \in (0 \dots N)) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ)$
498	478 483 497	sylc	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ$
499	498	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ$
500	42	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to x \in X$
501	499 500	ffvelrnd	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (S D^{n} H (Z)) (J - 1^{st} (p)) (x) \in ℂ$
502	468 501	mulcld	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) \in ℂ$
503	413 502	mulcld	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) \in ℂ$
504	338 380 382 388 503	fsumf1o	$⊢ (φ \land x \in X) \to \sum_{p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))} (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = \sum_{c \in C (R \cup \{Z\}) (J)} (\binom{J}{J - c (Z)}) (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x)$
505		simpl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to φ$
506	367	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R \cup \{Z\}) (J) = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
507	383 506	eleqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
508	375	sseli	$⊢ c \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \to c \in ({(0 \dots J)}^{(R \cup \{Z\})})$
509	507 508	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in ({(0 \dots J)}^{(R \cup \{Z\})})$
510		elmapi	$⊢ c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
511	509 510	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
512		snidg	$⊢ Z \in T \to Z \in \{Z\}$
513	31 512	syl	$⊢ φ \to Z \in \{Z\}$
514		elun2	$⊢ Z \in \{Z\} \to Z \in (R \cup \{Z\})$
515	513 514	syl	$⊢ φ \to Z \in (R \cup \{Z\})$
516	515	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in (R \cup \{Z\})$
517	511 516	ffvelrnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots J)$
518		0zd	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \in ℤ$
519	128	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℤ$
520		fzssz	$⊢ (0 \dots J) \subseteq ℤ$
521	520	sseli	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℤ$
522	521	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℤ$
523	519 522	zsubcld	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in ℤ$
524		elfzle2	$⊢ c (Z) \in (0 \dots J) \to c (Z) \leq J$
525	524	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \leq J$
526	164	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℝ$
527	522	zred	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℝ$
528	526 527	subge0d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq J - c (Z) \leftrightarrow c (Z) \leq J)$
529	525 528	mpbird	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq J - c (Z)$
530		elfzle1	$⊢ c (Z) \in (0 \dots J) \to 0 \leq c (Z)$
531	530	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq c (Z)$
532	526 527	subge02d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq c (Z) \leftrightarrow J - c (Z) \leq J)$
533	531 532	mpbid	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \leq J$
534	518 519 523 529 533	elfzd	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in (0 \dots J)$
535	505 517 534	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in (0 \dots J)$
536		bcval2	$⊢ J - c (Z) \in (0 \dots J) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
537	535 536	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
538	164	recnd	$⊢ φ \to J \in ℂ$
539	538	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℂ$
540		zsscn	$⊢ ℤ \subseteq ℂ$
541	520 540	sstri	$⊢ (0 \dots J) \subseteq ℂ$
542	541	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq ℂ$
543	542 517	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℂ$
544	539 543	nncand	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - (J - c (Z)) = c (Z)$
545	544	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! = c (Z)!$
546	545	oveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! (J - c (Z))! = c (Z)! (J - c (Z))!$
547	546	oveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!} = \frac{J!}{c (Z)! (J - c (Z))!}$
548	50	faccld	$⊢ φ \to J! \in ℕ$
549	548	nncnd	$⊢ φ \to J! \in ℂ$
550	549	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
551		elfznn0	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℕ_{0}$
552	517 551	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℕ_{0}$
553	552	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℕ$
554	553	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
555		elfznn0	$⊢ J - c (Z) \in (0 \dots J) \to J - c (Z) \in ℕ_{0}$
556	535 555	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in ℕ_{0}$
557	556	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℕ$
558	557	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
559	553	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
560	557	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
561	550 554 558 559 560	divdiv1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!} = \frac{J!}{c (Z)! (J - c (Z))!}$
562	561	eqcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \frac{J!}{c (Z)! (J - c (Z))!} = \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}$
563	537 547 562	3eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}$
564	563	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}$
565		fvres	$⊢ t \in R \to ({c ↾}_{R}) (t) = c (t)$
566	565	fveq2d	$⊢ t \in R \to ({c ↾}_{R}) (t)! = c (t)!$
567	566	prodeq2i	$⊢ \prod_{t \in R} ({c ↾}_{R}) (t)! = \prod_{t \in R} c (t)!$
568	567	oveq2i	$⊢ \frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!} = \frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}$
569	565	fveq2d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) = (S D^{n} H (t)) (c (t))$
570	569	fveq1d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
571	570	prodeq2i	$⊢ \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
572	568 571	oveq12i	$⊢ (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (\frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
573	572	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (\frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
574	573	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (\frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)$
575	558	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
576	505 16	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
577	79	ssriv	$⊢ (0 \dots J) \subseteq ℕ_{0}$
578	577	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq ℕ_{0}$
579	511	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
580		elun1	$⊢ t \in R \to t \in (R \cup \{Z\})$
581	580	adantl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in (R \cup \{Z\})$
582	579 581	ffvelrnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots J)$
583	578 582	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in ℕ_{0}$
584	583	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℕ$
585	584	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℂ$
586	576 585	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
587	586	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
588	17	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
589	505	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to φ$
590	505 22	sylan	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in T$
591	589 136	syl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq (0 \dots N)$
592	591 582	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots N)$
593	589 590 592 148	syl3anc	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
594	593	adantllr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
595	25	adantlr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to x \in X$
596	594 595	ffvelrnd	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (S D^{n} H (t)) (c (t)) (x) \in ℂ$
597	588 596	fprodcl	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
598	576 584	fprodnncl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℕ$
599		nnne0	$⊢ \prod_{t \in R} c (t)! \in ℕ \to \prod_{t \in R} c (t)! \neq 0$
600	598 599	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
601	600	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
602	575 587 597 601	div32d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}) \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) = (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!})$
603	574 602	eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!})$
604	544	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (J - (J - c (Z))) = (S D^{n} H (Z)) (c (Z))$
605	604	fveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (S D^{n} H (Z)) (c (Z)) (x)$
606	605	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (S D^{n} H (Z)) (c (Z)) (x)$
607	603 606	oveq12d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
608	597 587 601	divcld	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!} \in ℂ$
609	505 31	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
610	505 136	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq (0 \dots N)$
611	610 517	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots N)$
612	505 609 611	3jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (φ \land Z \in T \land c (Z) \in (0 \dots N))$
613		eleq1	$⊢ j = c (Z) \to (j \in (0 \dots N) \leftrightarrow c (Z) \in (0 \dots N))$
614	613	3anbi3d	$⊢ j = c (Z) \to ((φ \land Z \in T \land j \in (0 \dots N)) \leftrightarrow (φ \land Z \in T \land c (Z) \in (0 \dots N)))$
615		fveq2	$⊢ j = c (Z) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (c (Z))$
616	615	feq1d	$⊢ j = c (Z) \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ)$
617	614 616	imbi12d	$⊢ j = c (Z) \to (((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ) \leftrightarrow ((φ \land Z \in T \land c (Z) \in (0 \dots N)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ))$
618	617 496	vtoclg	$⊢ c (Z) \in (0 \dots J) \to ((φ \land Z \in T \land c (Z) \in (0 \dots N)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ)$
619	517 612 618	sylc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
620	619	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
621	42	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to x \in X$
622	620 621	ffvelrnd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) (x) \in ℂ$
623	575 608 622	mulassd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
624	607 623	eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
625	564 624	oveq12d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (\frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}) (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
626	549	ad2antrr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
627	554	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
628	559	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
629	626 627 628	divcld	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J!}{c (Z)!} \in ℂ$
630	608 622	mulcld	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) \in ℂ$
631	560	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
632	629 575 630 631	dmmcand	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}) (J - c (Z))! (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = (\frac{J!}{c (Z)!}) (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
633	597 622 587 601	div23d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (c (Z)) (x)}{\prod_{t \in R} c (t)!} = (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x)$
634	633	eqcomd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = \frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (c (Z)) (x)}{\prod_{t \in R} c (t)!}$
635		nfv	$⊢ Ⅎ t ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J))$
636		nfcv	$⊢ \underline{Ⅎ} t (S D^{n} H (Z)) (c (Z)) (x)$
637	609	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
638	20	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
639		fveq2	$⊢ t = Z \to c (t) = c (Z)$
640	180 639	fveq12d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) = (S D^{n} H (Z)) (c (Z))$
641	640	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) (x) = (S D^{n} H (Z)) (c (Z)) (x)$
642	635 636 588 637 638 596 641 622	fprodsplitsn	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x) = \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (c (Z)) (x)$
643	642	eqcomd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (c (Z)) (x) = \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
644	643	oveq1d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x) (S D^{n} H (Z)) (c (Z)) (x)}{\prod_{t \in R} c (t)!} = \frac{\prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}$
645	634 644	eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = \frac{\prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}$
646	645	oveq2d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{J!}{c (Z)!}) (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = (\frac{J!}{c (Z)!}) (\frac{\prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!})$
647	588 369 371	sylancl	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
648	505	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to φ$
649	348	sselda	$⊢ (φ \land t \in (R \cup \{Z\})) \to t \in T$
650	649	adantlr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to t \in T$
651	511 610	fssd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots N)$
652	651	ffvelrnda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots N)$
653	648 650 652 148	syl3anc	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
654	653	adantllr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
655	621	adantr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to x \in X$
656	654 655	ffvelrnd	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (S D^{n} H (t)) (c (t)) (x) \in ℂ$
657	647 656	fprodcl	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x) \in ℂ$
658	626 627 657 587 628 601	divmuldivd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{J!}{c (Z)!}) (\frac{\prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) = \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{c (Z)! \prod_{t \in R} c (t)!}$
659	554 586	mulcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \prod_{t \in R} c (t)! = \prod_{t \in R} c (t)! c (Z)!$
660		nfv	$⊢ Ⅎ t (φ \land c \in C (R \cup \{Z\}) (J))$
661		nfcv	$⊢ \underline{Ⅎ} t c (Z)!$
662	505 19	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
663	639	fveq2d	$⊢ t = Z \to c (t)! = c (Z)!$
664	660 661 576 609 662 585 663 554	fprodsplitsn	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! = \prod_{t \in R} c (t)! c (Z)!$
665	664	eqcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! c (Z)! = \prod_{t \in R \cup \{Z\}} c (t)!$
666	659 665	eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \prod_{t \in R} c (t)! = \prod_{t \in R \cup \{Z\}} c (t)!$
667	666	oveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{c (Z)! \prod_{t \in R} c (t)!} = \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R \cup \{Z\}} c (t)!}$
668	667	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{c (Z)! \prod_{t \in R} c (t)!} = \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R \cup \{Z\}} c (t)!}$
669	505 372	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
670	577	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (0 \dots J) \subseteq ℕ_{0}$
671	511	ffvelrnda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots J)$
672	670 671	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in ℕ_{0}$
673	672	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℕ$
674	673	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℂ$
675	669 674	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
676	675	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
677	673	nnne0d	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \neq 0$
678	669 674 677	fprodn0	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
679	678	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
680	626 657 676 679	div23d	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R \cup \{Z\}} c (t)!} = (\frac{J!}{\prod_{t \in R \cup \{Z\}} c (t)!}) \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
681		eqidd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \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{J!}{\prod_{t \in R \cup \{Z\}} c (t)!}) \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
682	668 680 681	3eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J! \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)}{c (Z)! \prod_{t \in R} c (t)!} = (\frac{J!}{\prod_{t \in R \cup \{Z\}} c (t)!}) \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
683	646 658 682	3eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\frac{J!}{c (Z)!}) (\frac{\prod_{t \in R} (S D^{n} H (t)) (c (t)) (x)}{\prod_{t \in R} c (t)!}) (S D^{n} H (Z)) (c (Z)) (x) = (\frac{J!}{\prod_{t \in R \cup \{Z\}} c (t)!}) \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
684	625 632 683	3eqtrd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x) = (\frac{J!}{\prod_{t \in R \cup \{Z\}} c (t)!}) \prod_{t \in R \cup \{Z\}} (S D^{n} H (t)) (c (t)) (x)$
685	684	sumeq2dv	$⊢ (φ \land x \in X) \to \sum_{c \in C (R \cup \{Z\}) (J)} (\binom{J}{J - c (Z)}) (\frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) (S D^{n} H (Z)) (J - (J - c (Z))) (x) = \sum_{c \in C (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)$
686	504 685	eqtrd	$⊢ (φ \land x \in X) \to \sum_{p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))} (\binom{J}{1^{st} (p)}) (\frac{1^{st} (p)!}{\prod_{t \in R} 2^{nd} (p) (t)!}) \prod_{t \in R} (S D^{n} H (t)) (2^{nd} (p) (t)) (x) (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = \sum_{c \in C (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)$
687	295 319 686	3eqtrd	$⊢ (φ \land x \in X) \to \sum_{k = 0}^{J} (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x) = \sum_{c \in C (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)$
688	687	mpteq2dva	$⊢ φ \to (x \in X ⟼ \sum_{k = 0}^{J} (\binom{J}{k}) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ \prod_{t \in R} H (t) (y))) (k)) (k) (x) (k \in (0 \dots J) ⟼ (S D^{n} (y \in X ⟼ H (Z) (y))) (k)) (J - k) (x)) = (x \in X ⟼ \sum_{c \in C (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))$
689	47 210 688	3eqtrd	$⊢ φ \to (S D^{n} (x \in X ⟼ \prod_{t \in R \cup \{Z\}} H (t) (x))) (J) = (x \in X ⟼ \sum_{c \in C (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))$

Metamath Proof Explorer

Theorem dvnprodlem2

Proof