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