dvnprodlem2

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

Metamath Proof Explorer

Theorem dvnprodlem2

Proof