Metamath Proof Explorer

Theorem dvnprodlem2

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

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

Proof

Step Hyp Ref Expression
1 dvnprodlem2.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnprodlem2.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvnprodlem2.t 
 |-  ( ph -> T e. Fin )
4 dvnprodlem2.h 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
5 dvnprodlem2.n 
 |-  ( ph -> N e. NN0 )
6 dvnprodlem2.dvnh 
 |-  ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
7 dvnprodlem2.c 
 |-  C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
8 dvnprodlem2.r 
 |-  ( ph -> R C_ T )
9 dvnprodlem2.z 
 |-  ( ph -> Z e. ( T \ R ) )
10 dvnprodlem2.ind 
 |-  ( ph -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
11 dvnprodlem2.j 
 |-  ( ph -> J e. ( 0 ... N ) )
12 dvnprodlem2.d 
 |-  D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
13 nfv 
 |-  F/ t ( ph /\ x e. X )
14 nfcv 
 |-  F/_ t ( ( H ` Z ) ` x )
15 ssfi 
 |-  ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
16 3 8 15 syl2anc 
 |-  ( ph -> R e. Fin )
17 16 adantr 
 |-  ( ( ph /\ x e. X ) -> R e. Fin )
18 9 adantr 
 |-  ( ( ph /\ x e. X ) -> Z e. ( T \ R ) )
19 9 eldifbd 
 |-  ( ph -> -. Z e. R )
20 19 adantr 
 |-  ( ( ph /\ x e. X ) -> -. Z e. R )
21 simpl 
 |-  ( ( ph /\ t e. R ) -> ph )
22 8 sselda 
 |-  ( ( ph /\ t e. R ) -> t e. T )
23 21 22 4 syl2anc 
 |-  ( ( ph /\ t e. R ) -> ( H ` t ) : X --> CC )
24 23 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( H ` t ) : X --> CC )
25 simplr 
 |-  ( ( ( ph /\ x e. X ) /\ t e. R ) -> x e. X )
26 24 25 ffvelrnd 
 |-  ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( ( H ` t ) ` x ) e. CC )
27 fveq2 
 |-  ( t = Z -> ( H ` t ) = ( H ` Z ) )
28 27 fveq1d 
 |-  ( t = Z -> ( ( H ` t ) ` x ) = ( ( H ` Z ) ` x ) )
29 id 
 |-  ( ph -> ph )
30 eldifi 
 |-  ( Z e. ( T \ R ) -> Z e. T )
31 9 30 syl 
 |-  ( ph -> Z e. T )
32 simpr 
 |-  ( ( ph /\ Z e. T ) -> Z e. T )
33 id 
 |-  ( ( ph /\ Z e. T ) -> ( ph /\ Z e. T ) )
34 eleq1 
 |-  ( t = Z -> ( t e. T <-> Z e. T ) )
35 34 anbi2d 
 |-  ( t = Z -> ( ( ph /\ t e. T ) <-> ( ph /\ Z e. T ) ) )
36 27 feq1d 
 |-  ( t = Z -> ( ( H ` t ) : X --> CC <-> ( H ` Z ) : X --> CC ) )
37 35 36 imbi12d 
 |-  ( t = Z -> ( ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC ) <-> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) ) )
38 37 4 vtoclg 
 |-  ( Z e. T -> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) )
39 32 33 38 sylc 
 |-  ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC )
40 29 31 39 syl2anc 
 |-  ( ph -> ( H ` Z ) : X --> CC )
41 40 adantr 
 |-  ( ( ph /\ x e. X ) -> ( H ` Z ) : X --> CC )
42 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
43 41 42 ffvelrnd 
 |-  ( ( ph /\ x e. X ) -> ( ( H ` Z ) ` x ) e. CC )
44 13 14 17 18 20 26 28 43 fprodsplitsn 
 |-  ( ( ph /\ x e. X ) -> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) = ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) )
45 44 mpteq2dva 
 |-  ( ph -> ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) = ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) )
46 45 oveq2d 
 |-  ( ph -> ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) = ( S Dn ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) ) )
47 46 fveq1d 
 |-  ( ph -> ( ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) ` J ) = ( ( S Dn ( x e. X |-> ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) ) ) ` J ) )
48 13 17 26 fprodclf 
 |-  ( ( ph /\ x e. X ) -> prod_ t e. R ( ( H ` t ) ` x ) e. CC )
49 elfznn0 
 |-  ( J e. ( 0 ... N ) -> J e. NN0 )
50 11 49 syl 
 |-  ( ph -> J e. NN0 )
51 eqid 
 |-  ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) )
52 eqid 
 |-  ( x e. X |-> ( ( H ` Z ) ` x ) ) = ( x e. X |-> ( ( H ` Z ) ` x ) )
53 oveq2 
 |-  ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
54 rabeq 
 |-  ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
55 53 54 syl 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } )
56 sumeq1 
 |-  ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
57 56 eqeq1d 
 |-  ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
58 57 rabbidv 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
59 55 58 eqtrd 
 |-  ( s = R -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
60 59 mpteq2dv 
 |-  ( s = R -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
61 ssexg 
 |-  ( ( R C_ T /\ T e. Fin ) -> R e. _V )
62 8 3 61 syl2anc 
 |-  ( ph -> R e. _V )
63 elpwg 
 |-  ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
64 62 63 syl 
 |-  ( ph -> ( R e. ~P T <-> R C_ T ) )
65 8 64 mpbird 
 |-  ( ph -> R e. ~P T )
66 65 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> R e. ~P T )
67 nn0ex 
 |-  NN0 e. _V
68 67 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
69 68 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
70 7 60 66 69 fvmptd3 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
71 oveq2 
 |-  ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
72 71 oveq1d 
 |-  ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
73 rabeq 
 |-  ( ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
74 72 73 syl 
 |-  ( n = k -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } )
75 eqeq2 
 |-  ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
76 75 rabbidv 
 |-  ( n = k -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
77 74 76 eqtrd 
 |-  ( n = k -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
78 77 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ n = k ) -> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
79 elfznn0 
 |-  ( k e. ( 0 ... J ) -> k e. NN0 )
80 79 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
81 fzfid 
 |-  ( ph -> ( 0 ... k ) e. Fin )
82 mapfi 
 |-  ( ( ( 0 ... k ) e. Fin /\ R e. Fin ) -> ( ( 0 ... k ) ^m R ) e. Fin )
83 81 16 82 syl2anc 
 |-  ( ph -> ( ( 0 ... k ) ^m R ) e. Fin )
84 83 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 ... k ) ^m R ) e. Fin )
85 ssrab2 
 |-  { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R )
86 85 a1i 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R ) )
87 84 86 ssexd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
88 70 78 80 87 fvmptd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
89 ssfi 
 |-  ( ( ( ( 0 ... k ) ^m R ) e. Fin /\ { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
90 83 85 89 sylancl 
 |-  ( ph -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
91 90 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
92 88 91 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) e. Fin )
93 92 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) -> ( ( C ` R ) ` k ) e. Fin )
94 79 faccld 
 |-  ( k e. ( 0 ... J ) -> ( ! ` k ) e. NN )
95 94 nncnd 
 |-  ( k e. ( 0 ... J ) -> ( ! ` k ) e. CC )
96 95 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ! ` k ) e. CC )
97 16 adantr 
 |-  ( ( ph /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
98 97 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
99 elfznn0 
 |-  ( z e. ( 0 ... k ) -> z e. NN0 )
100 99 ssriv 
 |-  ( 0 ... k ) C_ NN0
101 100 a1i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ NN0 )
102 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( C ` R ) ` k ) )
103 88 eleq2d 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( c e. ( ( C ` R ) ` k ) <-> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) )
104 103 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( c e. ( ( C ` R ) ` k ) <-> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } ) )
105 102 104 mpbid 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
106 85 sseli 
 |-  ( c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> c e. ( ( 0 ... k ) ^m R ) )
107 105 106 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( 0 ... k ) ^m R ) )
108 elmapi 
 |-  ( c e. ( ( 0 ... k ) ^m R ) -> c : R --> ( 0 ... k ) )
109 107 108 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c : R --> ( 0 ... k ) )
110 109 adantr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> c : R --> ( 0 ... k ) )
111 simpr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. R )
112 110 111 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... k ) )
113 101 112 sseldd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. NN0 )
114 113 faccld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. NN )
115 114 nncnd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. CC )
116 98 115 fprodcl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. CC )
117 114 nnne0d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) =/= 0 )
118 98 115 117 fprodn0 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
119 96 116 118 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
120 119 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
121 98 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
122 29 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ph )
123 122 22 sylancom 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. T )
124 elfzuz3 
 |-  ( k e. ( 0 ... J ) -> J e. ( ZZ>= ` k ) )
125 fzss2 
 |-  ( J e. ( ZZ>= ` k ) -> ( 0 ... k ) C_ ( 0 ... J ) )
126 124 125 syl 
 |-  ( k e. ( 0 ... J ) -> ( 0 ... k ) C_ ( 0 ... J ) )
127 126 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... J ) )
128 50 nn0zd 
 |-  ( ph -> J e. ZZ )
129 5 nn0zd 
 |-  ( ph -> N e. ZZ )
130 elfzle2 
 |-  ( J e. ( 0 ... N ) -> J <_ N )
131 11 130 syl 
 |-  ( ph -> J <_ N )
132 128 129 131 3jca 
 |-  ( ph -> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
133 eluz2 
 |-  ( N e. ( ZZ>= ` J ) <-> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
134 132 133 sylibr 
 |-  ( ph -> N e. ( ZZ>= ` J ) )
135 fzss2 
 |-  ( N e. ( ZZ>= ` J ) -> ( 0 ... J ) C_ ( 0 ... N ) )
136 134 135 syl 
 |-  ( ph -> ( 0 ... J ) C_ ( 0 ... N ) )
137 136 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... J ) C_ ( 0 ... N ) )
138 127 137 sstrd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... N ) )
139 138 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ ( 0 ... N ) )
140 139 112 sseldd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
141 140 adantllr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
142 fvex 
 |-  ( c ` t ) e. _V
143 eleq1 
 |-  ( j = ( c ` t ) -> ( j e. ( 0 ... N ) <-> ( c ` t ) e. ( 0 ... N ) ) )
144 143 3anbi3d 
 |-  ( j = ( c ` t ) -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) ) )
145 fveq2 
 |-  ( j = ( c ` t ) -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
146 145 feq1d 
 |-  ( j = ( c ` t ) -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC ) )
147 144 146 imbi12d 
 |-  ( j = ( c ` t ) -> ( ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC ) <-> ( ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC ) ) )
148 142 147 6 vtocl 
 |-  ( ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
149 122 123 141 148 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
150 simpllr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> x e. X )
151 149 150 ffvelrnd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
152 121 151 fprodcl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
153 120 152 mulcld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
154 93 153 fsumcl 
 |-  ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) -> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) e. CC )
155 154 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) : X --> CC )
156 10 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
157 0zd 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> 0 e. ZZ )
158 129 adantr 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> N e. ZZ )
159 elfzelz 
 |-  ( k e. ( 0 ... J ) -> k e. ZZ )
160 159 adantl 
 |-  ( ( ph /\ k e. ( 0 ... J ) ) -> k e. ZZ )
161 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 syl5eq 
 |-  ( 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 ffvelrnd 
 |-  ( ( ( 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 ffvelrnda 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) e. CC )
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 ffvelrnd 
 |-  ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) e. CC )
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 ffvelrnd 
 |-  ( ( 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 ffvelrnd 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( ( ( 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 ffvelrnd 
 |-  ( ( ( 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 ffvelrnda 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
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 ffvelrnda 
 |-  ( ( ( 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 ) ) ) )