Theorem dvnprodlem2

Description: Induction step for dvnprodlem2 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvnprodlem2.s	|- ( ph -> S e. { RR , CC } )
	dvnprodlem2.x	|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
	dvnprodlem2.t	|- ( ph -> T e. Fin )
	dvnprodlem2.h	|- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
	dvnprodlem2.n	|- ( ph -> N e. NN0 )
	dvnprodlem2.dvnh	|- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
	dvnprodlem2.c	|- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
	dvnprodlem2.r	|- ( ph -> R C_ T )
	dvnprodlem2.z	|- ( ph -> Z e. ( T \ R ) )
	dvnprodlem2.ind	|- ( ph -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
	dvnprodlem2.j	|- ( ph -> J e. ( 0 ... N ) )
	dvnprodlem2.d	|- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
Assertion	dvnprodlem2	|- ( ph -> ( ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) ` J ) = ( x e. X |-> sum_ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( ( ! ` J ) / prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( R u. { Z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )

Proof

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