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	157 158 160	3jca	$⊢ (φ \land k \in (0 \dots J)) \to (0 \in ℤ \land N \in ℤ \land k \in ℤ)$
162		elfzle1	$⊢ k \in (0 \dots J) \to 0 \leq k$
163	162	adantl	$⊢ (φ \land k \in (0 \dots J)) \to 0 \leq k$
164	160	zred	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℝ$
165	50	nn0red	$⊢ φ \to J \in ℝ$
166	165	adantr	$⊢ (φ \land k \in (0 \dots J)) \to J \in ℝ$
167	158	zred	$⊢ (φ \land k \in (0 \dots J)) \to N \in ℝ$
168		elfzle2	$⊢ k \in (0 \dots J) \to k \leq J$
169	168	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \leq J$
170	131	adantr	$⊢ (φ \land k \in (0 \dots J)) \to J \leq N$
171	164 166 167 169 170	letrd	$⊢ (φ \land k \in (0 \dots J)) \to k \leq N$
172	161 163 171	jca32	$⊢ (φ \land k \in (0 \dots J)) \to ((0 \in ℤ \land N \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq N))$
173		elfz2	$⊢ k \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq N))$
174	172 173	sylibr	$⊢ (φ \land k \in (0 \dots J)) \to k \in (0 \dots N)$
175		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))$
176	156 174 175	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))$
177	176	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 ⟶ ℂ)$
178	155 177	mpbird	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ \prod_{t \in R} H (t) (x))) (k) : X ⟶ ℂ$
179	31	adantr	$⊢ (φ \land k \in (0 \dots J)) \to Z \in T$
180		simpl	$⊢ (φ \land k \in (0 \dots J)) \to φ$
181	180 179 174	3jca	$⊢ (φ \land k \in (0 \dots J)) \to (φ \land Z \in T \land k \in (0 \dots N))$
182	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)))$
183	27	oveq2d	$⊢ t = Z \to S D^{n} H (t) = S D^{n} H (Z)$
184	183	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (k) = (S D^{n} H (Z)) (k)$
185	184	feq1d	$⊢ t = Z \to ((S D^{n} H (t)) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (k) : X ⟶ ℂ)$
186	182 185	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 ⟶ ℂ))$
187		eleq1	$⊢ j = k \to (j \in (0 \dots N) \leftrightarrow k \in (0 \dots N))$
188	187	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)))$
189		fveq2	$⊢ j = k \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (k)$
190	189	feq1d	$⊢ j = k \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (t)) (k) : X ⟶ ℂ)$
191	188 190	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 ⟶ ℂ))$
192	191 6	chvarvv	$⊢ (φ \land t \in T \land k \in (0 \dots N)) \to (S D^{n} H (t)) (k) : X ⟶ ℂ$
193	186 192	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T \land k \in (0 \dots N)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ)$
194	179 181 193	sylc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (k) : X ⟶ ℂ$
195	40	feqmptd	$⊢ φ \to H (Z) = (x \in X ⟼ H (Z) (x))$
196	195	eqcomd	$⊢ φ \to (x \in X ⟼ H (Z) (x)) = H (Z)$
197	196	oveq2d	$⊢ φ \to S D^{n} (x \in X ⟼ H (Z) (x)) = S D^{n} H (Z)$
198	197	fveq1d	$⊢ φ \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) = (S D^{n} H (Z)) (k)$
199	198	adantr	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) = (S D^{n} H (Z)) (k)$
200	199	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 ⟶ ℂ)$
201	194 200	mpbird	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} (x \in X ⟼ H (Z) (x))) (k) : X ⟶ ℂ$
202		fveq2	$⊢ y = x \to H (t) (y) = H (t) (x)$
203	202	prodeq2ad	$⊢ y = x \to \prod_{t \in R} H (t) (y) = \prod_{t \in R} H (t) (x)$
204	203	cbvmptv	$⊢ (y \in X ⟼ \prod_{t \in R} H (t) (y)) = (x \in X ⟼ \prod_{t \in R} H (t) (x))$
205	204	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))$
206	205	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)$
207	206	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))$
208		fveq2	$⊢ y = x \to H (Z) (y) = H (Z) (x)$
209	208	cbvmptv	$⊢ (y \in X ⟼ H (Z) (y)) = (x \in X ⟼ H (Z) (x))$
210	209	oveq2i	$⊢ S D^{n} (y \in X ⟼ H (Z) (y)) = S D^{n} (x \in X ⟼ H (Z) (x))$
211	210	fveq1i	$⊢ (S D^{n} (y \in X ⟼ H (Z) (y))) (k) = (S D^{n} (x \in X ⟼ H (Z) (x))) (k)$
212	211	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))$
213	1 2 48 43 50 51 52 178 201 207 212	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))$
214	206	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)$
215	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))$
216	180 174 215	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))$
217	214 216	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))$
218	217	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)))$
219		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$
220	2 219	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$
221	220	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$
222	218 221	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))$
223	222	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))$
224	223	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)$
225	42	adantr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to x \in X$
226	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 ℂ$
227		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))$
228	227	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)$
229	225 226 228	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)$
230	224 229	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)$
231		fveq2	$⊢ k = j \to (S D^{n} (y \in X ⟼ H (Z) (y))) (k) = (S D^{n} (y \in X ⟼ H (Z) (y))) (j)$
232	231	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))$
233	232	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))$
234	210 197	syl5eq	$⊢ φ \to S D^{n} (y \in X ⟼ H (Z) (y)) = S D^{n} H (Z)$
235	234	fveq1d	$⊢ φ \to (S D^{n} (y \in X ⟼ H (Z) (y))) (j) = (S D^{n} H (Z)) (j)$
236	235	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))$
237	233 236	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))$
238	237	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))$
239		fveq2	$⊢ j = J - k \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - k)$
240	239	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)$
241		0zd	$⊢ k \in (0 \dots J) \to 0 \in ℤ$
242		elfzel2	$⊢ k \in (0 \dots J) \to J \in ℤ$
243	242 159	zsubcld	$⊢ k \in (0 \dots J) \to J - k \in ℤ$
244	241 242 243	3jca	$⊢ k \in (0 \dots J) \to (0 \in ℤ \land J \in ℤ \land J - k \in ℤ)$
245	242	zred	$⊢ k \in (0 \dots J) \to J \in ℝ$
246	79	nn0red	$⊢ k \in (0 \dots J) \to k \in ℝ$
247	245 246	subge0d	$⊢ k \in (0 \dots J) \to (0 \leq J - k \leftrightarrow k \leq J)$
248	168 247	mpbird	$⊢ k \in (0 \dots J) \to 0 \leq J - k$
249	245 246	subge02d	$⊢ k \in (0 \dots J) \to (0 \leq k \leftrightarrow J - k \leq J)$
250	162 249	mpbid	$⊢ k \in (0 \dots J) \to J - k \leq J$
251	244 248 250	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))$
252	251	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))$
253		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))$
254	252 253	sylibr	$⊢ (φ \land k \in (0 \dots J)) \to J - k \in (0 \dots J)$
255		fvex	$⊢ (S D^{n} H (Z)) (J - k) \in V$
256	255	a1i	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) \in V$
257	238 240 254 256	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)$
258	257	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)$
259	258	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)$
260	230 259	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)$
261	260	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)$
262	92	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to C (R) (k) \in Fin$
263		ovex	$⊢ J - k \in V$
264		eleq1	$⊢ j = J - k \to (j \in (0 \dots J) \leftrightarrow J - k \in (0 \dots J))$
265	264	anbi2d	$⊢ j = J - k \to ((φ \land j \in (0 \dots J)) \leftrightarrow (φ \land J - k \in (0 \dots J)))$
266	239	feq1d	$⊢ j = J - k \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (J - k) : X ⟶ ℂ)$
267	265 266	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 ⟶ ℂ))$
268		eleq1	$⊢ k = j \to (k \in (0 \dots J) \leftrightarrow j \in (0 \dots J))$
269	268	anbi2d	$⊢ k = j \to ((φ \land k \in (0 \dots J)) \leftrightarrow (φ \land j \in (0 \dots J)))$
270		fveq2	$⊢ k = j \to (S D^{n} H (Z)) (k) = (S D^{n} H (Z)) (j)$
271	270	feq1d	$⊢ k = j \to ((S D^{n} H (Z)) (k) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
272	269 271	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 ⟶ ℂ))$
273	272 194	chvarvv	$⊢ (φ \land j \in (0 \dots J)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ$
274	263 267 273	vtocl	$⊢ (φ \land J - k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
275	180 254 274	syl2anc	$⊢ (φ \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
276	275	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) : X ⟶ ℂ$
277	276 225	ffvelrnd	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (S D^{n} H (Z)) (J - k) (x) \in ℂ$
278		anass	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \leftrightarrow (φ \land (k \in (0 \dots J) \land x \in X))$
279		ancom	$⊢ (k \in (0 \dots J) \land x \in X) \leftrightarrow (x \in X \land k \in (0 \dots J))$
280	279	anbi2i	$⊢ (φ \land (k \in (0 \dots J) \land x \in X)) \leftrightarrow (φ \land (x \in X \land k \in (0 \dots J)))$
281		anass	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \leftrightarrow (φ \land (x \in X \land k \in (0 \dots J)))$
282	281	bicomi	$⊢ (φ \land (x \in X \land k \in (0 \dots J))) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
283	280 282	bitri	$⊢ (φ \land (k \in (0 \dots J) \land x \in X)) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
284	278 283	bitri	$⊢ ((φ \land k \in (0 \dots J)) \land x \in X) \leftrightarrow ((φ \land x \in X) \land k \in (0 \dots J))$
285	284	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))$
286	285	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 ℂ)$
287	153 286	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 ℂ$
288	262 277 287	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)$
289	288	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)$
290	180 50	syl	$⊢ (φ \land k \in (0 \dots J)) \to J \in ℕ_{0}$
291	290 160	bccld	$⊢ (φ \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℕ_{0}$
292	291	nn0cnd	$⊢ (φ \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℂ$
293	292	adantlr	$⊢ ((φ \land x \in X) \land k \in (0 \dots J)) \to (\binom{J}{k}) \in ℂ$
294	277	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 ℂ$
295	287 294	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 ℂ$
296	262 293 295	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)$
297	261 289 296	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)$
298	297	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)$
299		vex	$⊢ k \in V$
300		vex	$⊢ c \in V$
301	299 300	op1std	$⊢ p = ⟨k, c⟩ \to 1^{st} (p) = k$
302	301	oveq2d	$⊢ p = ⟨k, c⟩ \to (\binom{J}{1^{st} (p)}) = (\binom{J}{k})$
303	301	fveq2d	$⊢ p = ⟨k, c⟩ \to 1^{st} (p)! = k!$
304	299 300	op2ndd	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) = c$
305	304	fveq1d	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) (t) = c (t)$
306	305	fveq2d	$⊢ p = ⟨k, c⟩ \to 2^{nd} (p) (t)! = c (t)!$
307	306	prodeq2ad	$⊢ p = ⟨k, c⟩ \to \prod_{t \in R} 2^{nd} (p) (t)! = \prod_{t \in R} c (t)!$
308	303 307	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)!}$
309	305	fveq2d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) = (S D^{n} H (t)) (c (t))$
310	309	fveq1d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (t)) (2^{nd} (p) (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
311	310	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)$
312	308 311	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)$
313	301	oveq2d	$⊢ p = ⟨k, c⟩ \to J - 1^{st} (p) = J - k$
314	313	fveq2d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) = (S D^{n} H (Z)) (J - k)$
315	314	fveq1d	$⊢ p = ⟨k, c⟩ \to (S D^{n} H (Z)) (J - 1^{st} (p)) (x) = (S D^{n} H (Z)) (J - k) (x)$
316	312 315	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)$
317	302 316	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)$
318		fzfid	$⊢ (φ \land x \in X) \to (0 \dots J) \in Fin$
319	293	adantrr	$⊢ ((φ \land x \in X) \land (k \in (0 \dots J) \land c \in C (R) (k))) \to (\binom{J}{k}) \in ℂ$
320	295	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 ℂ$
321	319 320	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 ℂ$
322	317 318 262 321	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)$
323		ovex	$⊢ J - c (Z) \in V$
324	300	resex	$⊢ {c ↾}_{R} \in V$
325	323 324	op1std	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 1^{st} (p) = J - c (Z)$
326	325	oveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to (\binom{J}{1^{st} (p)}) = (\binom{J}{J - c (Z)})$
327	325	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 1^{st} (p)! = (J - c (Z))!$
328	323 324	op2ndd	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) = {c ↾}_{R}$
329	328	fveq1d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) (t) = ({c ↾}_{R}) (t)$
330	329	fveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to 2^{nd} (p) (t)! = ({c ↾}_{R}) (t)!$
331	330	prodeq2ad	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to \prod_{t \in R} 2^{nd} (p) (t)! = \prod_{t \in R} ({c ↾}_{R}) (t)!$
332	327 331	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)!}$
333	329	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))$
334	333	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)$
335	334	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)$
336	332 335	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)$
337	325	oveq2d	$⊢ p = ⟨J - c (Z), {c ↾}_{R}⟩ \to J - 1^{st} (p) = J - (J - c (Z))$
338	337	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)))$
339	338	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)$
340	336 339	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)$
341	326 340	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)$
342		oveq2	$⊢ s = R \cup \{Z\} \to {(0 \dots n)}^{s} = {(0 \dots n)}^{(R \cup \{Z\})}$
343		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\}$
344	342 343	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\}$
345		sumeq1	$⊢ s = R \cup \{Z\} \to \sum_{t \in s} c (t) = \sum_{t \in R \cup \{Z\}} c (t)$
346	345	eqeq1d	$⊢ s = R \cup \{Z\} \to (\sum_{t \in s} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = n)$
347	346	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\}$
348	344 347	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\}$
349	348	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\})$
350	31	snssd	$⊢ φ \to \{Z\} \subseteq T$
351	8 350	unssd	$⊢ φ \to R \cup \{Z\} \subseteq T$
352	3 351	ssexd	$⊢ φ \to R \cup \{Z\} \in V$
353		elpwg	$⊢ R \cup \{Z\} \in V \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
354	352 353	syl	$⊢ φ \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
355	351 354	mpbird	$⊢ φ \to R \cup \{Z\} \in 𝒫 T$
356	67	mptex	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
357	356	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
358	7 349 355 357	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\})$
359		oveq2	$⊢ n = J \to (0 \dots n) = (0 \dots J)$
360	359	oveq1d	$⊢ n = J \to {(0 \dots n)}^{(R \cup \{Z\})} = {(0 \dots J)}^{(R \cup \{Z\})}$
361		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\}$
362	360 361	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\}$
363		eqeq2	$⊢ n = J \to (\sum_{t \in R \cup \{Z\}} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = J)$
364	363	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\}$
365	362 364	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\}$
366	365	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\}$
367		ovex	$⊢ {(0 \dots J)}^{(R \cup \{Z\})} \in V$
368	367	rabex	$⊢ \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
369	368	a1i	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
370	358 366 50 369	fvmptd	$⊢ φ \to C (R \cup \{Z\}) (J) = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
371		fzfid	$⊢ φ \to (0 \dots J) \in Fin$
372		snfi	$⊢ \{Z\} \in Fin$
373	372	a1i	$⊢ φ \to \{Z\} \in Fin$
374		unfi	$⊢ (R \in Fin \land \{Z\} \in Fin) \to R \cup \{Z\} \in Fin$
375	16 373 374	syl2anc	$⊢ φ \to R \cup \{Z\} \in Fin$
376		mapfi	$⊢ ((0 \dots J) \in Fin \land R \cup \{Z\} \in Fin) \to {(0 \dots J)}^{(R \cup \{Z\})} \in Fin$
377	371 375 376	syl2anc	$⊢ φ \to {(0 \dots J)}^{(R \cup \{Z\})} \in Fin$
378		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\})}$
379	378	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\})}$
380		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$
381	377 379 380	syl2anc	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in Fin$
382	370 381	eqeltrd	$⊢ φ \to C (R \cup \{Z\}) (J) \in Fin$
383	382	adantr	$⊢ (φ \land x \in X) \to C (R \cup \{Z\}) (J) \in Fin$
384	7 50 12 3 31 19 351	dvnprodlem1	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
385	384	adantr	$⊢ (φ \land x \in X) \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
386		simpr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in C (R \cup \{Z\}) (J)$
387		opex	$⊢ ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
388	387	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
389	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}⟩$
390	386 388 389	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
391	390	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
392	50	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J \in ℕ_{0}$
393		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))$
394	393	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))$
395	394	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))$
396		nfv	$⊢ Ⅎ k φ$
397		nfcv	$⊢ \underline{Ⅎ} k p$
398		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
399	397 398	nfel	$⊢ Ⅎ k p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
400	396 399	nfan	$⊢ Ⅎ k (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
401		nfv	$⊢ Ⅎ k 1^{st} (p) \in (0 \dots J)$
402		xp1st	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in \{k\}$
403		elsni	$⊢ 1^{st} (p) \in \{k\} \to 1^{st} (p) = k$
404	402 403	syl	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) = k$
405	404	adantl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) = k$
406		simpl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in (0 \dots J)$
407	405 406	eqeltrd	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
408	407	ex	$⊢ k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
409	408	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)))$
410	400 401 409	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))$
411	395 410	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
412		elfzelz	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℤ$
413	411 412	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℤ$
414	392 413	bccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℕ_{0}$
415	414	nn0cnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
416	415	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
417		elfznn0	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℕ_{0}$
418	411 417	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℕ_{0}$
419	418	faccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℕ$
420	419	nncnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
421	420	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
422	16	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
423		nfv	$⊢ Ⅎ k 2^{nd} (p) : R ⟶ (0 \dots J)$
424	88 86	eqsstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots k)}^{R}$
425		ovex	$⊢ (0 \dots J) \in V$
426	425	a1i	$⊢ k \in (0 \dots J) \to (0 \dots J) \in V$
427		mapss	$⊢ ((0 \dots J) \in V \land (0 \dots k) \subseteq (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
428	426 126 427	syl2anc	$⊢ k \in (0 \dots J) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
429	428	adantl	$⊢ (φ \land k \in (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
430	424 429	sstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
431	430	3adant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
432		xp2nd	$⊢ p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) \in C (R) (k)$
433	432	3ad2ant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in C (R) (k)$
434	431 433	sseldd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in ({(0 \dots J)}^{R})$
435		elmapi	$⊢ 2^{nd} (p) \in ({(0 \dots J)}^{R}) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
436	434 435	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
437	436	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) : R ⟶ (0 \dots J)))$
438	437	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)))$
439	400 423 438	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))$
440	395 439	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
441	440	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)$
442		elfznn0	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t) \in ℕ_{0}$
443	442	faccld	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℕ$
444	443	nncnd	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℂ$
445	441 444	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℂ$
446	422 445	fprodcl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \in ℂ$
447	446	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 ℂ$
448	441 443	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℕ$
449		nnne0	$⊢ 2^{nd} (p) (t)! \in ℕ \to 2^{nd} (p) (t)! \neq 0$
450	448 449	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \neq 0$
451	422 445 450	fprodn0	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \neq 0$
452	451	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$
453	421 447 452	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 ℂ$
454	17	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
455		simpll	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to φ$
456	455 22	sylancom	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to t \in T$
457	455 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)$
458	457 441	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)$
459	455 456 458	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))$
460		eleq1	$⊢ j = 2^{nd} (p) (t) \to (j \in (0 \dots N) \leftrightarrow 2^{nd} (p) (t) \in (0 \dots N))$
461	460	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)))$
462		fveq2	$⊢ j = 2^{nd} (p) (t) \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (2^{nd} (p) (t))$
463	462	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 ⟶ ℂ)$
464	461 463	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 ⟶ ℂ))$
465	464 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 ⟶ ℂ)$
466	441 459 465	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 ⟶ ℂ$
467	466	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 ⟶ ℂ$
468	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$
469	467 468	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 ℂ$
470	454 469	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 ℂ$
471	453 470	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 ℂ$
472		nfv	$⊢ Ⅎ k J - 1^{st} (p) \in (0 \dots J)$
473		simp1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to φ$
474	407	3adant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
475		fznn0sub2	$⊢ 1^{st} (p) \in (0 \dots J) \to J - 1^{st} (p) \in (0 \dots J)$
476	475	adantl	$⊢ (φ \land 1^{st} (p) \in (0 \dots J)) \to J - 1^{st} (p) \in (0 \dots J)$
477	473 474 476	syl2anc	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
478	477	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to J - 1^{st} (p) \in (0 \dots J)))$
479	478	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)))$
480	400 472 479	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))$
481	395 480	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
482		simpl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to φ$
483	482 31	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to Z \in T$
484	482 136	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (0 \dots J) \subseteq (0 \dots N)$
485	484 481	sseldd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots N)$
486	482 483 485	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))$
487		eleq1	$⊢ j = J - 1^{st} (p) \to (j \in (0 \dots N) \leftrightarrow J - 1^{st} (p) \in (0 \dots N))$
488	487	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)))$
489		fveq2	$⊢ j = J - 1^{st} (p) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - 1^{st} (p))$
490	489	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 ⟶ ℂ)$
491	488 490	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 ⟶ ℂ))$
492		simp2	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to Z \in T$
493		id	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (φ \land Z \in T \land j \in (0 \dots N))$
494	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)))$
495	183	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (j) = (S D^{n} H (Z)) (j)$
496	495	feq1d	$⊢ t = Z \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
497	494 496	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 ⟶ ℂ))$
498	497 6	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
499	492 493 498	sylc	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ$
500	491 499	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 ⟶ ℂ)$
501	481 486 500	sylc	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ$
502	501	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 ⟶ ℂ$
503	42	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to x \in X$
504	502 503	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 ℂ$
505	471 504	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 ℂ$
506	416 505	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 ℂ$
507	341 383 385 391 506	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)$
508		simpl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to φ$
509	370	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\}$
510	386 509	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\}$
511	378	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\})})$
512	510 511	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in ({(0 \dots J)}^{(R \cup \{Z\})})$
513		elmapi	$⊢ c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
514	512 513	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
515		snidg	$⊢ Z \in T \to Z \in \{Z\}$
516	31 515	syl	$⊢ φ \to Z \in \{Z\}$
517		elun2	$⊢ Z \in \{Z\} \to Z \in (R \cup \{Z\})$
518	516 517	syl	$⊢ φ \to Z \in (R \cup \{Z\})$
519	518	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in (R \cup \{Z\})$
520	514 519	ffvelrnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots J)$
521		0zd	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \in ℤ$
522	128	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℤ$
523		fzssz	$⊢ (0 \dots J) \subseteq ℤ$
524	523	sseli	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℤ$
525	524	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℤ$
526	522 525	zsubcld	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in ℤ$
527	521 522 526	3jca	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \in ℤ \land J \in ℤ \land J - c (Z) \in ℤ)$
528		elfzle2	$⊢ c (Z) \in (0 \dots J) \to c (Z) \leq J$
529	528	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \leq J$
530	165	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℝ$
531	525	zred	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℝ$
532	530 531	subge0d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq J - c (Z) \leftrightarrow c (Z) \leq J)$
533	529 532	mpbird	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq J - c (Z)$
534		elfzle1	$⊢ c (Z) \in (0 \dots J) \to 0 \leq c (Z)$
535	534	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq c (Z)$
536	530 531	subge02d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq c (Z) \leftrightarrow J - c (Z) \leq J)$
537	535 536	mpbid	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \leq J$
538	527 533 537	jca32	$⊢ (φ \land c (Z) \in (0 \dots J)) \to ((0 \in ℤ \land J \in ℤ \land J - c (Z) \in ℤ) \land (0 \leq J - c (Z) \land J - c (Z) \leq J))$
539		elfz2	$⊢ J - c (Z) \in (0 \dots J) \leftrightarrow ((0 \in ℤ \land J \in ℤ \land J - c (Z) \in ℤ) \land (0 \leq J - c (Z) \land J - c (Z) \leq J))$
540	538 539	sylibr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in (0 \dots J)$
541	508 520 540	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in (0 \dots J)$
542		bcval2	$⊢ J - c (Z) \in (0 \dots J) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
543	541 542	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
544	165	recnd	$⊢ φ \to J \in ℂ$
545	544	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℂ$
546		zsscn	$⊢ ℤ \subseteq ℂ$
547	523 546	sstri	$⊢ (0 \dots J) \subseteq ℂ$
548	547	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq ℂ$
549	548 520	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℂ$
550	545 549	nncand	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - (J - c (Z)) = c (Z)$
551	550	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! = c (Z)!$
552	551	oveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! (J - c (Z))! = c (Z)! (J - c (Z))!$
553	552	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))!}$
554	50	faccld	$⊢ φ \to J! \in ℕ$
555	554	nncnd	$⊢ φ \to J! \in ℂ$
556	555	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
557		elfznn0	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℕ_{0}$
558	520 557	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℕ_{0}$
559	558	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℕ$
560	559	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
561		elfznn0	$⊢ J - c (Z) \in (0 \dots J) \to J - c (Z) \in ℕ_{0}$
562	541 561	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in ℕ_{0}$
563	562	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℕ$
564	563	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
565	559	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
566	563	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
567	556 560 564 565 566	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))!}$
568	567	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))!}$
569	543 553 568	3eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}$
570	569	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))!}$
571		fvres	$⊢ t \in R \to ({c ↾}_{R}) (t) = c (t)$
572	571	fveq2d	$⊢ t \in R \to ({c ↾}_{R}) (t)! = c (t)!$
573	572	prodeq2i	$⊢ \prod_{t \in R} ({c ↾}_{R}) (t)! = \prod_{t \in R} c (t)!$
574	573	oveq2i	$⊢ \frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!} = \frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}$
575	571	fveq2d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) = (S D^{n} H (t)) (c (t))$
576	575	fveq1d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
577	576	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)$
578	574 577	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)$
579	578	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)$
580	579	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)$
581	564	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
582	508 16	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
583	79	ssriv	$⊢ (0 \dots J) \subseteq ℕ_{0}$
584	583	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq ℕ_{0}$
585	514	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
586		elun1	$⊢ t \in R \to t \in (R \cup \{Z\})$
587	586	adantl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in (R \cup \{Z\})$
588	585 587	ffvelrnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots J)$
589	584 588	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in ℕ_{0}$
590	589	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℕ$
591	590	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℂ$
592	582 591	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
593	592	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
594	17	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
595	508	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to φ$
596	508 22	sylan	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in T$
597	595 136	syl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq (0 \dots N)$
598	597 588	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots N)$
599	595 596 598 148	syl3anc	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
600	599	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 ⟶ ℂ$
601	25	adantlr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to x \in X$
602	600 601	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 ℂ$
603	594 602	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 ℂ$
604	582 590	fprodnncl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℕ$
605		nnne0	$⊢ \prod_{t \in R} c (t)! \in ℕ \to \prod_{t \in R} c (t)! \neq 0$
606	604 605	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
607	606	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
608	581 593 603 607	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)!})$
609	580 608	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)!})$
610	550	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))$
611	610	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)$
612	611	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)$
613	609 612	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)$
614	603 593 607	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 ℂ$
615	508 31	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
616	508 136	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq (0 \dots N)$
617	616 520	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots N)$
618	508 615 617	3jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (φ \land Z \in T \land c (Z) \in (0 \dots N))$
619		eleq1	$⊢ j = c (Z) \to (j \in (0 \dots N) \leftrightarrow c (Z) \in (0 \dots N))$
620	619	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)))$
621		fveq2	$⊢ j = c (Z) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (c (Z))$
622	621	feq1d	$⊢ j = c (Z) \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ)$
623	620 622	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 ⟶ ℂ))$
624	623 499	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 ⟶ ℂ)$
625	520 618 624	sylc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
626	625	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
627	42	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to x \in X$
628	626 627	ffvelrnd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) (x) \in ℂ$
629	581 614 628	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)$
630	613 629	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)$
631	570 630	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)$
632	555	ad2antrr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
633	560	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
634	565	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
635	632 633 634	divcld	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J!}{c (Z)!} \in ℂ$
636	614 628	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 ℂ$
637	566	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
638	635 581 636 637	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)$
639	603 628 593 607	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)$
640	639	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)!}$
641		nfv	$⊢ Ⅎ t ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J))$
642		nfcv	$⊢ \underline{Ⅎ} t (S D^{n} H (Z)) (c (Z)) (x)$
643	615	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
644	20	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
645		fveq2	$⊢ t = Z \to c (t) = c (Z)$
646	183 645	fveq12d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) = (S D^{n} H (Z)) (c (Z))$
647	646	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) (x) = (S D^{n} H (Z)) (c (Z)) (x)$
648	641 642 594 643 644 602 647 628	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)$
649	648	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)$
650	649	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)!}$
651	640 650	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)!}$
652	651	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)!})$
653	594 372 374	sylancl	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
654	508	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to φ$
655	351	sselda	$⊢ (φ \land t \in (R \cup \{Z\})) \to t \in T$
656	655	adantlr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to t \in T$
657	514 616	fssd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots N)$
658	657	ffvelrnda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots N)$
659	654 656 658 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 ⟶ ℂ$
660	659	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 ⟶ ℂ$
661	627	adantr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to x \in X$
662	660 661	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 ℂ$
663	653 662	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 ℂ$
664	632 633 663 593 634 607	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)!}$
665	560 592	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)!$
666		nfv	$⊢ Ⅎ t (φ \land c \in C (R \cup \{Z\}) (J))$
667		nfcv	$⊢ \underline{Ⅎ} t c (Z)!$
668	508 19	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
669	645	fveq2d	$⊢ t = Z \to c (t)! = c (Z)!$
670	666 667 582 615 668 591 669 560	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)!$
671	670	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)!$
672	665 671	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)!$
673	672	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)!}$
674	673	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)!}$
675	508 375	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
676	583	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (0 \dots J) \subseteq ℕ_{0}$
677	514	ffvelrnda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots J)$
678	676 677	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in ℕ_{0}$
679	678	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℕ$
680	679	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℂ$
681	675 680	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
682	681	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
683	679	nnne0d	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \neq 0$
684	675 680 683	fprodn0	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
685	684	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
686	632 663 682 685	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)$
687		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)$
688	674 686 687	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)$
689	652 664 688	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)$
690	631 638 689	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)$
691	690	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)$
692	507 691	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)$
693	298 322 692	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)$
694	693	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))$
695	47 213 694	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