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	ffvelcdmd	$⊢ ((φ \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	ffvelcdmd	$⊢ (φ \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	ffvelcdmd	$⊢ (((φ \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	ffvelcdmd	$⊢ ((((φ \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	eqtrid	$⊢ φ \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	ffvelcdmd	$⊢ ((φ \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	bilani	$⊢ (φ \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))$
392		nfv	$⊢ Ⅎ k φ$
393		nfcv	$⊢ \underline{Ⅎ} k p$
394		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
395	393 394	nfel	$⊢ Ⅎ k p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
396	392 395	nfan	$⊢ Ⅎ k (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
397		nfv	$⊢ Ⅎ k 1^{st} (p) \in (0 \dots J)$
398		xp1st	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in \{k\}$
399		elsni	$⊢ 1^{st} (p) \in \{k\} \to 1^{st} (p) = k$
400	398 399	syl	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) = k$
401	400	adantl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) = k$
402		simpl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in (0 \dots J)$
403	401 402	eqeltrd	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
404	403	ex	$⊢ k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
405	404	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)))$
406	396 397 405	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))$
407	391 406	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
408		elfzelz	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℤ$
409	407 408	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℤ$
410	389 409	bccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℕ_{0}$
411	410	nn0cnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
412	411	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\binom{J}{1^{st} (p)}) \in ℂ$
413		elfznn0	$⊢ 1^{st} (p) \in (0 \dots J) \to 1^{st} (p) \in ℕ_{0}$
414	407 413	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℕ_{0}$
415	414	faccld	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℕ$
416	415	nncnd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
417	416	adantlr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 1^{st} (p)! \in ℂ$
418	16	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
419		nfv	$⊢ Ⅎ k 2^{nd} (p) : R ⟶ (0 \dots J)$
420	88 86	eqsstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots k)}^{R}$
421		ovex	$⊢ (0 \dots J) \in V$
422	421	a1i	$⊢ k \in (0 \dots J) \to (0 \dots J) \in V$
423		mapss	$⊢ ((0 \dots J) \in V \land (0 \dots k) \subseteq (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
424	422 126 423	syl2anc	$⊢ k \in (0 \dots J) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
425	424	adantl	$⊢ (φ \land k \in (0 \dots J)) \to {(0 \dots k)}^{R} \subseteq {(0 \dots J)}^{R}$
426	420 425	sstrd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
427	426	3adant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to C (R) (k) \subseteq {(0 \dots J)}^{R}$
428		xp2nd	$⊢ p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) \in C (R) (k)$
429	428	3ad2ant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in C (R) (k)$
430	427 429	sseldd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in ({(0 \dots J)}^{R})$
431		elmapi	$⊢ 2^{nd} (p) \in ({(0 \dots J)}^{R}) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
432	430 431	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
433	432	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) : R ⟶ (0 \dots J)))$
434	433	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)))$
435	396 419 434	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))$
436	391 435	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots J)$
437	436	ffvelcdmda	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in (0 \dots J)$
438		elfznn0	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t) \in ℕ_{0}$
439	438	faccld	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℕ$
440	439	nncnd	$⊢ 2^{nd} (p) (t) \in (0 \dots J) \to 2^{nd} (p) (t)! \in ℂ$
441	437 440	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℂ$
442	418 441	fprodcl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \in ℂ$
443	442	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 ℂ$
444	437 439	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \in ℕ$
445		nnne0	$⊢ 2^{nd} (p) (t)! \in ℕ \to 2^{nd} (p) (t)! \neq 0$
446	444 445	syl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t)! \neq 0$
447	418 441 446	fprodn0	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \prod_{t \in R} 2^{nd} (p) (t)! \neq 0$
448	447	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$
449	417 443 448	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 ℂ$
450	17	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to R \in Fin$
451		simpll	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to φ$
452	451 22	sylancom	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land t \in R) \to t \in T$
453	451 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)$
454	453 437	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)$
455	451 452 454	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))$
456		eleq1	$⊢ j = 2^{nd} (p) (t) \to (j \in (0 \dots N) \leftrightarrow 2^{nd} (p) (t) \in (0 \dots N))$
457	456	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)))$
458		fveq2	$⊢ j = 2^{nd} (p) (t) \to (S D^{n} H (t)) (j) = (S D^{n} H (t)) (2^{nd} (p) (t))$
459	458	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 ⟶ ℂ)$
460	457 459	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 ⟶ ℂ))$
461	460 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 ⟶ ℂ)$
462	437 455 461	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 ⟶ ℂ$
463	462	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 ⟶ ℂ$
464	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$
465	463 464	ffvelcdmd	$⊢ (((φ \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 ℂ$
466	450 465	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 ℂ$
467	449 466	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 ℂ$
468		nfv	$⊢ Ⅎ k J - 1^{st} (p) \in (0 \dots J)$
469		simp1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to φ$
470	403	3adant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
471		fznn0sub2	$⊢ 1^{st} (p) \in (0 \dots J) \to J - 1^{st} (p) \in (0 \dots J)$
472	471	adantl	$⊢ (φ \land 1^{st} (p) \in (0 \dots J)) \to J - 1^{st} (p) \in (0 \dots J)$
473	469 470 472	syl2anc	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
474	473	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to J - 1^{st} (p) \in (0 \dots J)))$
475	474	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)))$
476	396 468 475	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))$
477	391 476	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots J)$
478		simpl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to φ$
479	478 31	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to Z \in T$
480	478 136	syl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (0 \dots J) \subseteq (0 \dots N)$
481	480 477	sseldd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in (0 \dots N)$
482	478 479 481	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))$
483		eleq1	$⊢ j = J - 1^{st} (p) \to (j \in (0 \dots N) \leftrightarrow J - 1^{st} (p) \in (0 \dots N))$
484	483	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)))$
485		fveq2	$⊢ j = J - 1^{st} (p) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (J - 1^{st} (p))$
486	485	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 ⟶ ℂ)$
487	484 486	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 ⟶ ℂ))$
488		simp2	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to Z \in T$
489		id	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (φ \land Z \in T \land j \in (0 \dots N))$
490	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)))$
491	180	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (j) = (S D^{n} H (Z)) (j)$
492	491	feq1d	$⊢ t = Z \to ((S D^{n} H (t)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
493	490 492	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 ⟶ ℂ))$
494	493 6	vtoclg	$⊢ Z \in T \to ((φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ)$
495	488 489 494	sylc	$⊢ (φ \land Z \in T \land j \in (0 \dots N)) \to (S D^{n} H (Z)) (j) : X ⟶ ℂ$
496	487 495	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 ⟶ ℂ)$
497	477 482 496	sylc	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (S D^{n} H (Z)) (J - 1^{st} (p)) : X ⟶ ℂ$
498	497	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 ⟶ ℂ$
499	42	adantr	$⊢ ((φ \land x \in X) \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to x \in X$
500	498 499	ffvelcdmd	$⊢ ((φ \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 ℂ$
501	467 500	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 ℂ$
502	412 501	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 ℂ$
503	338 380 382 388 502	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)$
504		simpl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to φ$
505	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\}$
506	383 505	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\}$
507	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\})})$
508	506 507	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in ({(0 \dots J)}^{(R \cup \{Z\})})$
509		elmapi	$⊢ c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
510	508 509	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
511		snidg	$⊢ Z \in T \to Z \in \{Z\}$
512	31 511	syl	$⊢ φ \to Z \in \{Z\}$
513		elun2	$⊢ Z \in \{Z\} \to Z \in (R \cup \{Z\})$
514	512 513	syl	$⊢ φ \to Z \in (R \cup \{Z\})$
515	514	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in (R \cup \{Z\})$
516	510 515	ffvelcdmd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots J)$
517		0zd	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \in ℤ$
518	128	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℤ$
519		fzssz	$⊢ (0 \dots J) \subseteq ℤ$
520	519	sseli	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℤ$
521	520	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℤ$
522	518 521	zsubcld	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in ℤ$
523		elfzle2	$⊢ c (Z) \in (0 \dots J) \to c (Z) \leq J$
524	523	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \leq J$
525	164	adantr	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J \in ℝ$
526	521	zred	$⊢ (φ \land c (Z) \in (0 \dots J)) \to c (Z) \in ℝ$
527	525 526	subge0d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq J - c (Z) \leftrightarrow c (Z) \leq J)$
528	524 527	mpbird	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq J - c (Z)$
529		elfzle1	$⊢ c (Z) \in (0 \dots J) \to 0 \leq c (Z)$
530	529	adantl	$⊢ (φ \land c (Z) \in (0 \dots J)) \to 0 \leq c (Z)$
531	525 526	subge02d	$⊢ (φ \land c (Z) \in (0 \dots J)) \to (0 \leq c (Z) \leftrightarrow J - c (Z) \leq J)$
532	530 531	mpbid	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \leq J$
533	517 518 522 528 532	elfzd	$⊢ (φ \land c (Z) \in (0 \dots J)) \to J - c (Z) \in (0 \dots J)$
534	504 516 533	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in (0 \dots J)$
535		bcval2	$⊢ J - c (Z) \in (0 \dots J) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
536	534 535	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{J!}{(J - (J - c (Z)))! (J - c (Z))!}$
537	164	recnd	$⊢ φ \to J \in ℂ$
538	537	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℂ$
539		zsscn	$⊢ ℤ \subseteq ℂ$
540	519 539	sstri	$⊢ (0 \dots J) \subseteq ℂ$
541	540	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq ℂ$
542	541 516	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℂ$
543	538 542	nncand	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - (J - c (Z)) = c (Z)$
544	543	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! = c (Z)!$
545	544	oveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - (J - c (Z)))! (J - c (Z))! = c (Z)! (J - c (Z))!$
546	545	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))!}$
547	50	faccld	$⊢ φ \to J! \in ℕ$
548	547	nncnd	$⊢ φ \to J! \in ℂ$
549	548	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
550		elfznn0	$⊢ c (Z) \in (0 \dots J) \to c (Z) \in ℕ_{0}$
551	516 550	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℕ_{0}$
552	551	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℕ$
553	552	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
554		elfznn0	$⊢ J - c (Z) \in (0 \dots J) \to J - c (Z) \in ℕ_{0}$
555	534 554	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in ℕ_{0}$
556	555	faccld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℕ$
557	556	nncnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
558	552	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
559	556	nnne0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
560	549 553 557 558 559	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))!}$
561	560	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))!}$
562	536 546 561	3eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (\binom{J}{J - c (Z)}) = \frac{\frac{J!}{c (Z)!}}{(J - c (Z))!}$
563	562	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))!}$
564		fvres	$⊢ t \in R \to ({c ↾}_{R}) (t) = c (t)$
565	564	fveq2d	$⊢ t \in R \to ({c ↾}_{R}) (t)! = c (t)!$
566	565	prodeq2i	$⊢ \prod_{t \in R} ({c ↾}_{R}) (t)! = \prod_{t \in R} c (t)!$
567	566	oveq2i	$⊢ \frac{(J - c (Z))!}{\prod_{t \in R} ({c ↾}_{R}) (t)!} = \frac{(J - c (Z))!}{\prod_{t \in R} c (t)!}$
568	564	fveq2d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) = (S D^{n} H (t)) (c (t))$
569	568	fveq1d	$⊢ t \in R \to (S D^{n} H (t)) (({c ↾}_{R}) (t)) (x) = (S D^{n} H (t)) (c (t)) (x)$
570	569	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)$
571	567 570	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)$
572	571	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)$
573	572	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)$
574	557	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \in ℂ$
575	504 16	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
576	79	ssriv	$⊢ (0 \dots J) \subseteq ℕ_{0}$
577	576	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq ℕ_{0}$
578	510	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
579		elun1	$⊢ t \in R \to t \in (R \cup \{Z\})$
580	579	adantl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in (R \cup \{Z\})$
581	578 580	ffvelcdmd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots J)$
582	577 581	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in ℕ_{0}$
583	582	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℕ$
584	583	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t)! \in ℂ$
585	575 584	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
586	585	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℂ$
587	17	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
588	504	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to φ$
589	504 22	sylan	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in T$
590	588 136	syl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (0 \dots J) \subseteq (0 \dots N)$
591	590 581	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots N)$
592	588 589 591 148	syl3anc	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to (S D^{n} H (t)) (c (t)) : X ⟶ ℂ$
593	592	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 ⟶ ℂ$
594	25	adantlr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to x \in X$
595	593 594	ffvelcdmd	$⊢ (((φ \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 ℂ$
596	587 595	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 ℂ$
597	575 583	fprodnncl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \in ℕ$
598		nnne0	$⊢ \prod_{t \in R} c (t)! \in ℕ \to \prod_{t \in R} c (t)! \neq 0$
599	597 598	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
600	599	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R} c (t)! \neq 0$
601	574 586 596 600	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)!})$
602	573 601	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)!})$
603	543	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))$
604	603	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)$
605	604	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)$
606	602 605	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)$
607	596 586 600	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 ℂ$
608	504 31	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
609	504 136	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq (0 \dots N)$
610	609 516	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots N)$
611	504 608 610	3jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (φ \land Z \in T \land c (Z) \in (0 \dots N))$
612		eleq1	$⊢ j = c (Z) \to (j \in (0 \dots N) \leftrightarrow c (Z) \in (0 \dots N))$
613	612	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)))$
614		fveq2	$⊢ j = c (Z) \to (S D^{n} H (Z)) (j) = (S D^{n} H (Z)) (c (Z))$
615	614	feq1d	$⊢ j = c (Z) \to ((S D^{n} H (Z)) (j) : X ⟶ ℂ \leftrightarrow (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ)$
616	613 615	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 ⟶ ℂ))$
617	616 495	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 ⟶ ℂ)$
618	516 611 617	sylc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
619	618	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) : X ⟶ ℂ$
620	42	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to x \in X$
621	619 620	ffvelcdmd	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (S D^{n} H (Z)) (c (Z)) (x) \in ℂ$
622	574 607 621	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)$
623	606 622	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)$
624	563 623	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)$
625	548	ad2antrr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to J! \in ℂ$
626	553	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \in ℂ$
627	558	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to c (Z)! \neq 0$
628	625 626 627	divcld	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \frac{J!}{c (Z)!} \in ℂ$
629	607 621	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 ℂ$
630	559	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z))! \neq 0$
631	628 574 629 630	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)$
632	596 621 586 600	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)$
633	632	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)!}$
634		nfv	$⊢ Ⅎ t ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J))$
635		nfcv	$⊢ \underline{Ⅎ} t (S D^{n} H (Z)) (c (Z)) (x)$
636	608	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
637	20	adantr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
638		fveq2	$⊢ t = Z \to c (t) = c (Z)$
639	180 638	fveq12d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) = (S D^{n} H (Z)) (c (Z))$
640	639	fveq1d	$⊢ t = Z \to (S D^{n} H (t)) (c (t)) (x) = (S D^{n} H (Z)) (c (Z)) (x)$
641	634 635 587 636 637 595 640 621	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)$
642	641	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)$
643	642	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)!}$
644	633 643	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)!}$
645	644	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)!})$
646	587 369 371	sylancl	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
647	504	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to φ$
648	348	sselda	$⊢ (φ \land t \in (R \cup \{Z\})) \to t \in T$
649	648	adantlr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to t \in T$
650	510 609	fssd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots N)$
651	650	ffvelcdmda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots N)$
652	647 649 651 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 ⟶ ℂ$
653	652	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 ⟶ ℂ$
654	620	adantr	$⊢ (((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to x \in X$
655	653 654	ffvelcdmd	$⊢ (((φ \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 ℂ$
656	646 655	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 ℂ$
657	625 626 656 586 627 600	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)!}$
658	553 585	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)!$
659		nfv	$⊢ Ⅎ t (φ \land c \in C (R \cup \{Z\}) (J))$
660		nfcv	$⊢ \underline{Ⅎ} t c (Z)!$
661	504 19	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
662	638	fveq2d	$⊢ t = Z \to c (t)! = c (Z)!$
663	659 660 575 608 661 584 662 553	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)!$
664	663	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)!$
665	658 664	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)!$
666	665	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)!}$
667	666	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)!}$
668	504 372	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \cup \{Z\} \in Fin$
669	576	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to (0 \dots J) \subseteq ℕ_{0}$
670	510	ffvelcdmda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in (0 \dots J)$
671	669 670	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t) \in ℕ_{0}$
672	671	faccld	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℕ$
673	672	nncnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \in ℂ$
674	668 673	fprodcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
675	674	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \in ℂ$
676	672	nnne0d	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in (R \cup \{Z\})) \to c (t)! \neq 0$
677	668 673 676	fprodn0	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
678	677	adantlr	$⊢ ((φ \land x \in X) \land c \in C (R \cup \{Z\}) (J)) \to \prod_{t \in R \cup \{Z\}} c (t)! \neq 0$
679	625 656 675 678	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)$
680		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)$
681	667 679 680	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)$
682	645 657 681	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)$
683	624 631 682	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)$
684	683	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)$
685	503 684	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)$
686	295 319 685	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)$
687	686	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))$
688	47 210 687	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