Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem2 Structured version   Visualization version   Unicode version
Theorem dvnprodlem2 40162
Description: Induction step for dvnprodlem2 40162. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem2.s |- ( ph -> S e. { RR , CC } )
dvnprodlem2.x |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾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
Ref Expression
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 ) ) ) )
Distinct variable groups:   x, k   C, c, k, t   D, c, t   H, c, j, k, t   x, H, c, t   J, c, j, k, t   n, J, s, c, k, t   x, J   j, N, t   R, c, k, n, s, t   x, R   S, c, j, k, t   x, S   T, j, t   T, s   X, c, j, k, t   x, X   Z, c, j, k, t   n, Z, s   x, Z   ph, c, j, k, t   ph, n, s   ph, x
Allowed substitution hints:   C( x, j, n, s)   D( x, j, k, n, s)   R( j)   S( n, s)   T( x, k, n, c)   H( n, s)   N( x, k, n, s, c)   X( n, s)
Proof of Theorem dvnprodlem2
Dummy variables p y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1843 . . . . . 6 |- F/ t ( ph /\ x e. X )
2 nfcv 2764 . . . . . 6 |- F/_ t ( ( H ` Z ) ` x )
3 dvnprodlem2.t . . . . . . . 8 |- ( ph -> T e. Fin )
4 dvnprodlem2.r . . . . . . . 8 |- ( ph -> R C_ T )
5 ssfi 8180 . . . . . . . 8 |- ( ( T e. Fin /\ R C_ T ) -> R e. Fin )
63, 4, 5syl2anc 693 . . . . . . 7 |- ( ph -> R e. Fin )
76adantr 481 . . . . . 6 |- ( ( ph /\ x e. X ) -> R e. Fin )
8 dvnprodlem2.z . . . . . . 7 |- ( ph -> Z e. ( T \ R ) )
98adantr 481 . . . . . 6 |- ( ( ph /\ x e. X ) -> Z e. ( T \ R ) )
108eldifbd 3587 . . . . . . 7 |- ( ph -> -. Z e. R )
1110adantr 481 . . . . . 6 |- ( ( ph /\ x e. X ) -> -. Z e. R )
12 simpl 473 . . . . . . . . 9 |- ( ( ph /\ t e. R ) -> ph )
134sselda 3603 . . . . . . . . 9 |- ( ( ph /\ t e. R ) -> t e. T )
14 dvnprodlem2.h . . . . . . . . 9 |- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
1512, 13, 14syl2anc 693 . . . . . . . 8 |- ( ( ph /\ t e. R ) -> ( H ` t ) : X --> CC )
1615adantlr 751 . . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( H ` t ) : X --> CC )
17 simplr 792 . . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> x e. X )
1816, 17ffvelrnd 6360 . . . . . 6 |- ( ( ( ph /\ x e. X ) /\ t e. R ) -> ( ( H ` t ) ` x ) e. CC )
19 fveq2 6191 . . . . . . 7 |- ( t = Z -> ( H ` t ) = ( H ` Z ) )
2019fveq1d 6193 . . . . . 6 |- ( t = Z -> ( ( H ` t ) ` x ) = ( ( H ` Z ) ` x ) )
21 id 22 . . . . . . . . 9 |- ( ph -> ph )
22 eldifi 3732 . . . . . . . . . 10 |- ( Z e. ( T \ R ) -> Z e. T )
238, 22syl 17 . . . . . . . . 9 |- ( ph -> Z e. T )
24 simpr 477 . . . . . . . . . 10 |- ( ( ph /\ Z e. T ) -> Z e. T )
25 id 22 . . . . . . . . . 10 |- ( ( ph /\ Z e. T ) -> ( ph /\ Z e. T ) )
26 eleq1 2689 . . . . . . . . . . . . 13 |- ( t = Z -> ( t e. T <-> Z e. T ) )
2726anbi2d 740 . . . . . . . . . . . 12 |- ( t = Z -> ( ( ph /\ t e. T ) <-> ( ph /\ Z e. T ) ) )
2819feq1d 6030 . . . . . . . . . . . 12 |- ( t = Z -> ( ( H ` t ) : X --> CC <-> ( H ` Z ) : X --> CC ) )
2927, 28imbi12d 334 . . . . . . . . . . 11 |- ( t = Z -> ( ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC ) <-> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) ) )
3029, 14vtoclg 3266 . . . . . . . . . 10 |- ( Z e. T -> ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC ) )
3124, 25, 30sylc 65 . . . . . . . . 9 |- ( ( ph /\ Z e. T ) -> ( H ` Z ) : X --> CC )
3221, 23, 31syl2anc 693 . . . . . . . 8 |- ( ph -> ( H ` Z ) : X --> CC )
3332adantr 481 . . . . . . 7 |- ( ( ph /\ x e. X ) -> ( H ` Z ) : X --> CC )
34 simpr 477 . . . . . . 7 |- ( ( ph /\ x e. X ) -> x e. X )
3533, 34ffvelrnd 6360 . . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( H ` Z ) ` x ) e. CC )
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 14720 . . . . 5 |- ( ( ph /\ x e. X ) -> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) = ( prod_ t e. R ( ( H ` t ) ` x ) x. ( ( H ` Z ) ` x ) ) )
3736mpteq2dva 4744 . . . 4 |- ( 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 ) ) ) )
3837oveq2d 6666 . . 3 |- ( 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 ) ) ) ) )
3938fveq1d 6193 . 2 |- ( 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 ) )
40 dvnprodlem2.s . . 3 |- ( ph -> S e. { RR , CC } )
41 dvnprodlem2.x . . 3 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
421, 7, 18fprodclf 14723 . . 3 |- ( ( ph /\ x e. X ) -> prod_ t e. R ( ( H ` t ) ` x ) e. CC )
43 dvnprodlem2.j . . . 4 |- ( ph -> J e. ( 0 ... N ) )
44 elfznn0 12433 . . . 4 |- ( J e. ( 0 ... N ) -> J e. NN0 )
4543, 44syl 17 . . 3 |- ( ph -> J e. NN0 )
46 eqid 2622 . . 3 |- ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) )
47 eqid 2622 . . 3 |- ( x e. X |-> ( ( H ` Z ) ` x ) ) = ( x e. X |-> ( ( H ` Z ) ` x ) )
48 dvnprodlem2.c . . . . . . . . . . 11 |- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
4948a1i 11 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) ) )
50 oveq2 6658 . . . . . . . . . . . . . 14 |- ( s = R -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m R ) )
51 rabeq 3192 . . . . . . . . . . . . . 14 |- ( ( ( 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 } )
5250, 51syl 17 . . . . . . . . . . . . 13 |- ( 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 } )
53 sumeq1 14419 . . . . . . . . . . . . . . 15 |- ( s = R -> sum_ t e. s ( c ` t ) = sum_ t e. R ( c ` t ) )
5453eqeq1d 2624 . . . . . . . . . . . . . 14 |- ( s = R -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = n ) )
5554rabbidv 3189 . . . . . . . . . . . . 13 |- ( 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 } )
5652, 55eqtrd 2656 . . . . . . . . . . . 12 |- ( 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 } )
5756mpteq2dv 4745 . . . . . . . . . . 11 |- ( 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 } ) )
5857adantl 482 . . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ 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 } ) )
59 ssexg 4804 . . . . . . . . . . . . . 14 |- ( ( R C_ T /\ T e. Fin ) -> R e. _V )
604, 3, 59syl2anc 693 . . . . . . . . . . . . 13 |- ( ph -> R e. _V )
61 elpwg 4166 . . . . . . . . . . . . 13 |- ( R e. _V -> ( R e. ~P T <-> R C_ T ) )
6260, 61syl 17 . . . . . . . . . . . 12 |- ( ph -> ( R e. ~P T <-> R C_ T ) )
634, 62mpbird 247 . . . . . . . . . . 11 |- ( ph -> R e. ~P T )
6463adantr 481 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> R e. ~P T )
65 nn0ex 11298 . . . . . . . . . . . 12 |- NN0 e. _V
6665mptex 6486 . . . . . . . . . . 11 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V
6766a1i 11 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) e. _V )
6849, 58, 64, 67fvmptd 6288 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( C ` R ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m R ) | sum_ t e. R ( c ` t ) = n } ) )
69 oveq2 6658 . . . . . . . . . . . . 13 |- ( n = k -> ( 0 ... n ) = ( 0 ... k ) )
7069oveq1d 6665 . . . . . . . . . . . 12 |- ( n = k -> ( ( 0 ... n ) ^m R ) = ( ( 0 ... k ) ^m R ) )
71 rabeq 3192 . . . . . . . . . . . 12 |- ( ( ( 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 } )
7270, 71syl 17 . . . . . . . . . . 11 |- ( 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 } )
73 eqeq2 2633 . . . . . . . . . . . 12 |- ( n = k -> ( sum_ t e. R ( c ` t ) = n <-> sum_ t e. R ( c ` t ) = k ) )
7473rabbidv 3189 . . . . . . . . . . 11 |- ( 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 } )
7572, 74eqtrd 2656 . . . . . . . . . 10 |- ( 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 } )
7675adantl 482 . . . . . . . . 9 |- ( ( ( 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 } )
77 elfznn0 12433 . . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k e. NN0 )
7877adantl 482 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. NN0 )
79 fzfid 12772 . . . . . . . . . . . 12 |- ( ph -> ( 0 ... k ) e. Fin )
80 mapfi 8262 . . . . . . . . . . . 12 |- ( ( ( 0 ... k ) e. Fin /\ R e. Fin ) -> ( ( 0 ... k ) ^m R ) e. Fin )
8179, 6, 80syl2anc 693 . . . . . . . . . . 11 |- ( ph -> ( ( 0 ... k ) ^m R ) e. Fin )
8281adantr 481 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 ... k ) ^m R ) e. Fin )
83 ssrab2 3687 . . . . . . . . . . 11 |- { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R )
8483a1i 11 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } C_ ( ( 0 ... k ) ^m R ) )
8582, 84ssexd 4805 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. _V )
8668, 76, 78, 85fvmptd 6288 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) = { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } )
87 ssfi 8180 . . . . . . . . . 10 |- ( ( ( ( 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 )
8881, 83, 87sylancl 694 . . . . . . . . 9 |- ( ph -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
8988adantr 481 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } e. Fin )
9086, 89eqeltrd 2701 . . . . . . 7 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) e. Fin )
9190adantr 481 . . . . . 6 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) -> ( ( C ` R ) ` k ) e. Fin )
9277faccld 13071 . . . . . . . . . . 11 |- ( k e. ( 0 ... J ) -> ( ! ` k ) e. NN )
9392nncnd 11036 . . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> ( ! ` k ) e. CC )
9493ad2antlr 763 . . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ! ` k ) e. CC )
956adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
9695adantlr 751 . . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
97 elfznn0 12433 . . . . . . . . . . . . . . 15 |- ( z e. ( 0 ... k ) -> z e. NN0 )
9897ssriv 3607 . . . . . . . . . . . . . 14 |- ( 0 ... k ) C_ NN0
9998a1i 11 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ NN0 )
100 simpr 477 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( C ` R ) ` k ) )
10186eleq2d 2687 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 } ) )
102101adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 } ) )
103100, 102mpbid 222 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 } )
10483sseli 3599 . . . . . . . . . . . . . . . . 17 |- ( c e. { c e. ( ( 0 ... k ) ^m R ) | sum_ t e. R ( c ` t ) = k } -> c e. ( ( 0 ... k ) ^m R ) )
105103, 104syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c e. ( ( 0 ... k ) ^m R ) )
106 elmapi 7879 . . . . . . . . . . . . . . . 16 |- ( c e. ( ( 0 ... k ) ^m R ) -> c : R --> ( 0 ... k ) )
107105, 106syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> c : R --> ( 0 ... k ) )
108107adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> c : R --> ( 0 ... k ) )
109 simpr 477 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. R )
110108, 109ffvelrnd 6360 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... k ) )
11199, 110sseldd 3604 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. NN0 )
112111faccld 13071 . . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. NN )
113112nncnd 11036 . . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. CC )
11496, 113fprodcl 14682 . . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. CC )
115112nnne0d 11065 . . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) =/= 0 )
11696, 113, 115fprodn0 14709 . . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
11794, 114, 116divcld 10801 . . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
118117adantlr 751 . . . . . . 7 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) e. CC )
11996adantlr 751 . . . . . . . 8 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) -> R e. Fin )
12021ad4antr 768 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ph )
121120, 13sylancom 701 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> t e. T )
122 elfzuz3 12339 . . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> J e. ( ZZ>= ` k ) )
123 fzss2 12381 . . . . . . . . . . . . . . . 16 |- ( J e. ( ZZ>= ` k ) -> ( 0 ... k ) C_ ( 0 ... J ) )
124122, 123syl 17 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 ... k ) C_ ( 0 ... J ) )
125124adantl 482 . . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... J ) )
12645nn0zd 11480 . . . . . . . . . . . . . . . . . 18 |- ( ph -> J e. ZZ )
127 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. NN0 )
128127nn0zd 11480 . . . . . . . . . . . . . . . . . 18 |- ( ph -> N e. ZZ )
129 elfzle2 12345 . . . . . . . . . . . . . . . . . . 19 |- ( J e. ( 0 ... N ) -> J <_ N )
13043, 129syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ph -> J <_ N )
131126, 128, 1303jca 1242 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
132 eluz2 11693 . . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` J ) <-> ( J e. ZZ /\ N e. ZZ /\ J <_ N ) )
133131, 132sylibr 224 . . . . . . . . . . . . . . . 16 |- ( ph -> N e. ( ZZ>= ` J ) )
134 fzss2 12381 . . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` J ) -> ( 0 ... J ) C_ ( 0 ... N ) )
135133, 134syl 17 . . . . . . . . . . . . . . 15 |- ( ph -> ( 0 ... J ) C_ ( 0 ... N ) )
136135adantr 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... J ) C_ ( 0 ... N ) )
137125, 136sstrd 3613 . . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 ... k ) C_ ( 0 ... N ) )
138137ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( 0 ... k ) C_ ( 0 ... N ) )
139138, 110sseldd 3604 . . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
140139adantllr 755 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
141 fvex 6201 . . . . . . . . . . 11 |- ( c ` t ) e. _V
142 eleq1 2689 . . . . . . . . . . . . 13 |- ( j = ( c ` t ) -> ( j e. ( 0 ... N ) <-> ( c ` t ) e. ( 0 ... N ) ) )
1431423anbi3d 1405 . . . . . . . . . . . 12 |- ( j = ( c ` t ) -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) ) )
144 fveq2 6191 . . . . . . . . . . . . 13 |- ( j = ( c ` t ) -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
145144feq1d 6030 . . . . . . . . . . . 12 |- ( j = ( c ` t ) -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC ) )
146143, 145imbi12d 334 . . . . . . . . . . 11 |- ( 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 ) ) )
147 dvnprodlem2.dvnh . . . . . . . . . . 11 |- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
148141, 146, 147vtocl 3259 . . . . . . . . . 10 |- ( ( ph /\ t e. T /\ ( c ` t ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
149120, 121, 140, 148syl3anc 1326 . . . . . . . . 9 |- ( ( ( ( ( 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 799 . . . . . . . . 9 |- ( ( ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) /\ c e. ( ( C ` R ) ` k ) ) /\ t e. R ) -> x e. X )
151149, 150ffvelrnd 6360 . . . . . . . 8 |- ( ( ( ( ( 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 )
152119, 151fprodcl 14682 . . . . . . 7 |- ( ( ( ( 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 )
153118, 152mulcld 10060 . . . . . 6 |- ( ( ( ( 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 )
15491, 153fsumcl 14464 . . . . 5 |- ( ( ( 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 eqid 2622 . . . . 5 |- ( 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 ) ) )
156154, 155fmptd 6385 . . . 4 |- ( ( 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 )
157 dvnprodlem2.ind . . . . . . 7 |- ( 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 ) ) ) )
158157adantr 481 . . . . . 6 |- ( ( 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 ) ) ) )
159 0zd 11389 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> 0 e. ZZ )
160128adantr 481 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> N e. ZZ )
161 elfzelz 12342 . . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k e. ZZ )
162161adantl 482 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. ZZ )
163159, 160, 1623jca 1242 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
164 elfzle1 12344 . . . . . . . . 9 |- ( k e. ( 0 ... J ) -> 0 <_ k )
165164adantl 482 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> 0 <_ k )
166162zred 11482 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. RR )
16745nn0red 11352 . . . . . . . . . 10 |- ( ph -> J e. RR )
168167adantr 481 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J e. RR )
169160zred 11482 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> N e. RR )
170 elfzle2 12345 . . . . . . . . . 10 |- ( k e. ( 0 ... J ) -> k <_ J )
171170adantl 482 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k <_ J )
172130adantr 481 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J <_ N )
173166, 168, 169, 171, 172letrd 10194 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k <_ N )
174163, 165, 173jca32 558 . . . . . . 7 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
175 elfz2 12333 . . . . . . 7 |- ( k e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
176174, 175sylibr 224 . . . . . 6 |- ( ( ph /\ k e. ( 0 ... J ) ) -> k e. ( 0 ... N ) )
177 rspa 2930 . . . . . 6 |- ( ( 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 ) ) ) )
178158, 176, 177syl2anc 693 . . . . 5 |- ( ( 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 ) ) ) )
179178feq1d 6030 . . . 4 |- ( ( 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 ) )
180156, 179mpbird 247 . . 3 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) : X --> CC )
18123adantr 481 . . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> Z e. T )
182 simpl 473 . . . . . 6 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ph )
183182, 181, 1763jca 1242 . . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) )
184263anbi2d 1404 . . . . . . 7 |- ( t = Z -> ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) <-> ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) ) )
18519oveq2d 6666 . . . . . . . . 9 |- ( t = Z -> ( S Dn ( H ` t ) ) = ( S Dn ( H ` Z ) ) )
186185fveq1d 6193 . . . . . . . 8 |- ( t = Z -> ( ( S Dn ( H ` t ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
187186feq1d 6030 . . . . . . 7 |- ( t = Z -> ( ( ( S Dn ( H ` t ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
188184, 187imbi12d 334 . . . . . 6 |- ( 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 ) ) )
189 eleq1 2689 . . . . . . . . 9 |- ( j = k -> ( j e. ( 0 ... N ) <-> k e. ( 0 ... N ) ) )
1901893anbi3d 1405 . . . . . . . 8 |- ( j = k -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ k e. ( 0 ... N ) ) ) )
191 fveq2 6191 . . . . . . . . 9 |- ( j = k -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` k ) )
192191feq1d 6030 . . . . . . . 8 |- ( j = k -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC ) )
193190, 192imbi12d 334 . . . . . . 7 |- ( 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 ) ) )
194193, 147chvarv 2263 . . . . . 6 |- ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC )
195188, 194vtoclg 3266 . . . . 5 |- ( Z e. T -> ( ( ph /\ Z e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
196181, 183, 195sylc 65 . . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC )
19732feqmptd 6249 . . . . . . . . 9 |- ( ph -> ( H ` Z ) = ( x e. X |-> ( ( H ` Z ) ` x ) ) )
198197eqcomd 2628 . . . . . . . 8 |- ( ph -> ( x e. X |-> ( ( H ` Z ) ` x ) ) = ( H ` Z ) )
199198oveq2d 6666 . . . . . . 7 |- ( ph -> ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) = ( S Dn ( H ` Z ) ) )
200199fveq1d 6193 . . . . . 6 |- ( ph -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
201200adantr 481 . . . . 5 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` k ) )
202201feq1d 6030 . . . 4 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC ) )
203196, 202mpbird 247 . . 3 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k ) : X --> CC )
204 fveq2 6191 . . . . . . . 8 |- ( y = x -> ( ( H ` t ) ` y ) = ( ( H ` t ) ` x ) )
205204prodeq2ad 39824 . . . . . . 7 |- ( y = x -> prod_ t e. R ( ( H ` t ) ` y ) = prod_ t e. R ( ( H ` t ) ` x ) )
206205cbvmptv 4750 . . . . . 6 |- ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) = ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) )
207206oveq2i 6661 . . . . 5 |- ( S Dn ( y e. X |-> prod_ t e. R ( ( H ` t ) ` y ) ) ) = ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) )
208207fveq1i 6192 . . . 4 |- ( ( 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 )
209208mpteq2i 4741 . . 3 |- ( 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 ) )
210 fveq2 6191 . . . . . . 7 |- ( y = x -> ( ( H ` Z ) ` y ) = ( ( H ` Z ) ` x ) )
211210cbvmptv 4750 . . . . . 6 |- ( y e. X |-> ( ( H ` Z ) ` y ) ) = ( x e. X |-> ( ( H ` Z ) ` x ) )
212211oveq2i 6661 . . . . 5 |- ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) = ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) )
213212fveq1i 6192 . . . 4 |- ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( ( H ` Z ) ` x ) ) ) ` k )
214213mpteq2i 4741 . . 3 |- ( 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 ) )
21540, 41, 42, 35, 45, 46, 47, 180, 203, 209, 214dvnmul 40158 . 2 |- ( 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 ) ) ) ) )
216208a1i 11 . . . . . . . . . . . . . 14 |- ( ( 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 ) )
217157r19.21bi 2932 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
218182, 176, 217syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
219216, 218eqtrd 2656 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
220219mpteq2dva 4744 . . . . . . . . . . . 12 |- ( 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 ) ) ) ) )
221 mptexg 6484 . . . . . . . . . . . . . 14 |- ( X e. ( ( TopOpen ` ℂfld ) ↾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 )
22241, 221syl 17 . . . . . . . . . . . . 13 |- ( 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 )
223222adantr 481 . . . . . . . . . . . 12 |- ( ( 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 )
224220, 223fvmpt2d 6293 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
225224adantlr 751 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
226225fveq1d 6193 . . . . . . . . 9 |- ( ( ( 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 ) )
22734adantr 481 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> x e. X )
228154an32s 846 . . . . . . . . . 10 |- ( ( ( 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 )
229155fvmpt2 6291 . . . . . . . . . 10 |- ( ( 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 ) ) )
230227, 228, 229syl2anc 693 . . . . . . . . 9 |- ( ( ( 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 ) ) )
231226, 230eqtrd 2656 . . . . . . . 8 |- ( ( ( 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 ) ) )
232 fveq2 6191 . . . . . . . . . . . . . . 15 |- ( k = j -> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) = ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) )
233232cbvmptv 4750 . . . . . . . . . . . . . 14 |- ( 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 ) )
234233a1i 11 . . . . . . . . . . . . 13 |- ( 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 ) ) )
235212, 199syl5eq 2668 . . . . . . . . . . . . . . 15 |- ( ph -> ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) = ( S Dn ( H ` Z ) ) )
236235fveq1d 6193 . . . . . . . . . . . . . 14 |- ( ph -> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` j ) )
237236mpteq2dv 4745 . . . . . . . . . . . . 13 |- ( ph -> ( j e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` j ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( H ` Z ) ) ` j ) ) )
238234, 237eqtrd 2656 . . . . . . . . . . . 12 |- ( ph -> ( k e. ( 0 ... J ) |-> ( ( S Dn ( y e. X |-> ( ( H ` Z ) ` y ) ) ) ` k ) ) = ( j e. ( 0 ... J ) |-> ( ( S Dn ( H ` Z ) ) ` j ) ) )
239238adantr 481 . . . . . . . . . . 11 |- ( ( 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 ) ) )
240 fveq2 6191 . . . . . . . . . . . 12 |- ( j = ( J - k ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
241240adantl 482 . . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ j = ( J - k ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
242 0zd 11389 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> 0 e. ZZ )
243 elfzel2 12340 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> J e. ZZ )
244243, 161zsubcld 11487 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( J - k ) e. ZZ )
245242, 243, 2443jca 1242 . . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) )
246243zred 11482 . . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> J e. RR )
24777nn0red 11352 . . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... J ) -> k e. RR )
248246, 247subge0d 10617 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 <_ ( J - k ) <-> k <_ J ) )
249170, 248mpbird 247 . . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> 0 <_ ( J - k ) )
250246, 247subge02d 10619 . . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... J ) -> ( 0 <_ k <-> ( J - k ) <_ J ) )
251164, 250mpbid 222 . . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> ( J - k ) <_ J )
252245, 249, 251jca32 558 . . . . . . . . . . . . 13 |- ( k e. ( 0 ... J ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
253252adantl 482 . . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
254 elfz2 12333 . . . . . . . . . . . 12 |- ( ( J - k ) e. ( 0 ... J ) <-> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - k ) e. ZZ ) /\ ( 0 <_ ( J - k ) /\ ( J - k ) <_ J ) ) )
255253, 254sylibr 224 . . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J - k ) e. ( 0 ... J ) )
256 fvex 6201 . . . . . . . . . . . 12 |- ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) e. _V
257256a1i 11 . . . . . . . . . . 11 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) e. _V )
258239, 241, 255, 257fvmptd 6288 . . . . . . . . . 10 |- ( ( 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 ) ) )
259258adantlr 751 . . . . . . . . 9 |- ( ( ( 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 ) ) )
260259fveq1d 6193 . . . . . . . 8 |- ( ( ( 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 ) )
261231, 260oveq12d 6668 . . . . . . 7 |- ( ( ( 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 ) ) )
262261oveq2d 6666 . . . . . 6 |- ( ( ( 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 ) ) ) )
26390adantlr 751 . . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) e. Fin )
264 ovex 6678 . . . . . . . . . . . 12 |- ( J - k ) e. _V
265 eleq1 2689 . . . . . . . . . . . . . 14 |- ( j = ( J - k ) -> ( j e. ( 0 ... J ) <-> ( J - k ) e. ( 0 ... J ) ) )
266265anbi2d 740 . . . . . . . . . . . . 13 |- ( j = ( J - k ) -> ( ( ph /\ j e. ( 0 ... J ) ) <-> ( ph /\ ( J - k ) e. ( 0 ... J ) ) ) )
267240feq1d 6030 . . . . . . . . . . . . 13 |- ( j = ( J - k ) -> ( ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC ) )
268266, 267imbi12d 334 . . . . . . . . . . . 12 |- ( 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 ) ) )
269 eleq1 2689 . . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. ( 0 ... J ) <-> j e. ( 0 ... J ) ) )
270269anbi2d 740 . . . . . . . . . . . . . 14 |- ( k = j -> ( ( ph /\ k e. ( 0 ... J ) ) <-> ( ph /\ j e. ( 0 ... J ) ) ) )
271 fveq2 6191 . . . . . . . . . . . . . . 15 |- ( k = j -> ( ( S Dn ( H ` Z ) ) ` k ) = ( ( S Dn ( H ` Z ) ) ` j ) )
272271feq1d 6030 . . . . . . . . . . . . . 14 |- ( k = j -> ( ( ( S Dn ( H ` Z ) ) ` k ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) )
273270, 272imbi12d 334 . . . . . . . . . . . . 13 |- ( 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 ) ) )
274273, 196chvarv 2263 . . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC )
275264, 268, 274vtocl 3259 . . . . . . . . . . 11 |- ( ( ph /\ ( J - k ) e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
276182, 255, 275syl2anc 693 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
277276adantlr 751 . . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) : X --> CC )
278277, 227ffvelrnd 6360 . . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) e. CC )
279 anass 681 . . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) <-> ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) )
280 ancom 466 . . . . . . . . . . . . . 14 |- ( ( k e. ( 0 ... J ) /\ x e. X ) <-> ( x e. X /\ k e. ( 0 ... J ) ) )
281280anbi2i 730 . . . . . . . . . . . . 13 |- ( ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) <-> ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) )
282 anass 681 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) <-> ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) )
283282bicomi 214 . . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. X /\ k e. ( 0 ... J ) ) ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
284281, 283bitri 264 . . . . . . . . . . . 12 |- ( ( ph /\ ( k e. ( 0 ... J ) /\ x e. X ) ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
285279, 284bitri 264 . . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... J ) ) /\ x e. X ) <-> ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) )
286285anbi1i 731 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
287286imbi1i 339 . . . . . . . . 9 |- ( ( ( ( ( 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 ) )
288153, 287mpbi 220 . . . . . . . 8 |- ( ( ( ( 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 )
289263, 278, 288fsummulc1 14517 . . . . . . 7 |- ( ( ( 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 ) ) )
290289oveq2d 6666 . . . . . 6 |- ( ( ( 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 ) ) ) )
291182, 45syl 17 . . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... J ) ) -> J e. NN0 )
292291, 162bccld 39531 . . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. NN0 )
293292nn0cnd 11353 . . . . . . . 8 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. CC )
294293adantlr 751 . . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) -> ( J _C k ) e. CC )
295278adantr 481 . . . . . . . 8 |- ( ( ( ( ph /\ x e. X ) /\ k e. ( 0 ... J ) ) /\ c e. ( ( C ` R ) ` k ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) e. CC )
296288, 295mulcld 10060 . . . . . . 7 |- ( ( ( ( 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 )
297263, 294, 296fsummulc2 14516 . . . . . 6 |- ( ( ( 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 ) ) ) )
298262, 290, 2973eqtrd 2660 . . . . 5 |- ( ( ( 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 ) ) ) )
299298sumeq2dv 14433 . . . 4 |- ( ( 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 ) ) ) )
300 vex 3203 . . . . . . . 8 |- k e. _V
301 vex 3203 . . . . . . . 8 |- c e. _V
302300, 301op1std 7178 . . . . . . 7 |- ( p = <. k , c >. -> ( 1st ` p ) = k )
303302oveq2d 6666 . . . . . 6 |- ( p = <. k , c >. -> ( J _C ( 1st ` p ) ) = ( J _C k ) )
304302fveq2d 6195 . . . . . . . . 9 |- ( p = <. k , c >. -> ( ! ` ( 1st ` p ) ) = ( ! ` k ) )
305300, 301op2ndd 7179 . . . . . . . . . . . 12 |- ( p = <. k , c >. -> ( 2nd ` p ) = c )
306305fveq1d 6193 . . . . . . . . . . 11 |- ( p = <. k , c >. -> ( ( 2nd ` p ) ` t ) = ( c ` t ) )
307306fveq2d 6195 . . . . . . . . . 10 |- ( p = <. k , c >. -> ( ! ` ( ( 2nd ` p ) ` t ) ) = ( ! ` ( c ` t ) ) )
308307prodeq2ad 39824 . . . . . . . . 9 |- ( p = <. k , c >. -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) = prod_ t e. R ( ! ` ( c ` t ) ) )
309304, 308oveq12d 6668 . . . . . . . 8 |- ( p = <. k , c >. -> ( ( ! ` ( 1st ` p ) ) / prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) ) = ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) )
310306fveq2d 6195 . . . . . . . . . 10 |- ( p = <. k , c >. -> ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
311310fveq1d 6193 . . . . . . . . 9 |- ( p = <. k , c >. -> ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
312311prodeq2ad 39824 . . . . . . . 8 |- ( 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 ) )
313309, 312oveq12d 6668 . . . . . . 7 |- ( 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 ) ) )
314302oveq2d 6666 . . . . . . . . 9 |- ( p = <. k , c >. -> ( J - ( 1st ` p ) ) = ( J - k ) )
315314fveq2d 6195 . . . . . . . 8 |- ( p = <. k , c >. -> ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) = ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) )
316315fveq1d 6193 . . . . . . 7 |- ( p = <. k , c >. -> ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( J - k ) ) ` x ) )
317313, 316oveq12d 6668 . . . . . 6 |- ( 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 ) ) )
318303, 317oveq12d 6668 . . . . 5 |- ( 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 ) ) ) )
319 fzfid 12772 . . . . 5 |- ( ( ph /\ x e. X ) -> ( 0 ... J ) e. Fin )
320294adantrr 753 . . . . . 6 |- ( ( ( ph /\ x e. X ) /\ ( k e. ( 0 ... J ) /\ c e. ( ( C ` R ) ` k ) ) ) -> ( J _C k ) e. CC )
321296anasss 679 . . . . . 6 |- ( ( ( 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 )
322320, 321mulcld 10060 . . . . 5 |- ( ( ( 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 )
323318, 319, 263, 322fsum2d 14502 . . . 4 |- ( ( 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 ) ) ) )
324 ovex 6678 . . . . . . . . 9 |- ( J - ( c ` Z ) ) e. _V
325301resex 5443 . . . . . . . . 9 |- ( c |` R ) e. _V
326324, 325op1std 7178 . . . . . . . 8 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( 1st ` p ) = ( J - ( c ` Z ) ) )
327326oveq2d 6666 . . . . . . 7 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( J _C ( 1st ` p ) ) = ( J _C ( J - ( c ` Z ) ) ) )
328326fveq2d 6195 . . . . . . . . . 10 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ! ` ( 1st ` p ) ) = ( ! ` ( J - ( c ` Z ) ) ) )
329324, 325op2ndd 7179 . . . . . . . . . . . . 13 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( 2nd ` p ) = ( c |` R ) )
330329fveq1d 6193 . . . . . . . . . . . 12 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ( 2nd ` p ) ` t ) = ( ( c |` R ) ` t ) )
331330fveq2d 6195 . . . . . . . . . . 11 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ! ` ( ( 2nd ` p ) ` t ) ) = ( ! ` ( ( c |` R ) ` t ) ) )
332331prodeq2ad 39824 . . . . . . . . . 10 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) = prod_ t e. R ( ! ` ( ( c |` R ) ` t ) ) )
333328, 332oveq12d 6668 . . . . . . . . 9 |- ( 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 ) ) ) )
334330fveq2d 6195 . . . . . . . . . . 11 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) = ( ( S Dn ( H ` t ) ) ` ( ( c |` R ) ` t ) ) )
335334fveq1d 6193 . . . . . . . . . 10 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( ( c |` R ) ` t ) ) ` x ) )
336335prodeq2ad 39824 . . . . . . . . 9 |- ( 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 ) )
337333, 336oveq12d 6668 . . . . . . . 8 |- ( 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 ) ) )
338326oveq2d 6666 . . . . . . . . . 10 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( J - ( 1st ` p ) ) = ( J - ( J - ( c ` Z ) ) ) )
339338fveq2d 6195 . . . . . . . . 9 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) = ( ( S Dn ( H ` Z ) ) ` ( J - ( J - ( c ` Z ) ) ) ) )
340339fveq1d 6193 . . . . . . . 8 |- ( p = <. ( J - ( c ` Z ) ) , ( c |` R ) >. -> ( ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( J - ( J - ( c ` Z ) ) ) ) ` x ) )
341337, 340oveq12d 6668 . . . . . . 7 |- ( 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 ) ) )
342327, 341oveq12d 6668 . . . . . 6 |- ( 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 ) ) ) )
34348a1i 11 . . . . . . . . . 10 |- ( ph -> C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) ) )
344 oveq2 6658 . . . . . . . . . . . . . 14 |- ( s = ( R u. { Z } ) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m ( R u. { Z } ) ) )
345 rabeq 3192 . . . . . . . . . . . . . 14 |- ( ( ( 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 } )
346344, 345syl 17 . . . . . . . . . . . . 13 |- ( 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 } )
347 sumeq1 14419 . . . . . . . . . . . . . . 15 |- ( s = ( R u. { Z } ) -> sum_ t e. s ( c ` t ) = sum_ t e. ( R u. { Z } ) ( c ` t ) )
348347eqeq1d 2624 . . . . . . . . . . . . . 14 |- ( s = ( R u. { Z } ) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = n ) )
349348rabbidv 3189 . . . . . . . . . . . . 13 |- ( 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 } )
350346, 349eqtrd 2656 . . . . . . . . . . . 12 |- ( 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 } )
351350mpteq2dv 4745 . . . . . . . . . . 11 |- ( 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 } ) )
352351adantl 482 . . . . . . . . . 10 |- ( ( ph /\ 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 } ) )
35323snssd 4340 . . . . . . . . . . . 12 |- ( ph -> { Z } C_ T )
3544, 353unssd 3789 . . . . . . . . . . 11 |- ( ph -> ( R u. { Z } ) C_ T )
3553, 354ssexd 4805 . . . . . . . . . . . 12 |- ( ph -> ( R u. { Z } ) e. _V )
356 elpwg 4166 . . . . . . . . . . . 12 |- ( ( R u. { Z } ) e. _V -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
357355, 356syl 17 . . . . . . . . . . 11 |- ( ph -> ( ( R u. { Z } ) e. ~P T <-> ( R u. { Z } ) C_ T ) )
358354, 357mpbird 247 . . . . . . . . . 10 |- ( ph -> ( R u. { Z } ) e. ~P T )
35965mptex 6486 . . . . . . . . . . 11 |- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V
360359a1i 11 . . . . . . . . . 10 |- ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = n } ) e. _V )
361343, 352, 358, 360fvmptd 6288 . . . . . . . . 9 |- ( 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 } ) )
362 oveq2 6658 . . . . . . . . . . . . 13 |- ( n = J -> ( 0 ... n ) = ( 0 ... J ) )
363362oveq1d 6665 . . . . . . . . . . . 12 |- ( n = J -> ( ( 0 ... n ) ^m ( R u. { Z } ) ) = ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
364 rabeq 3192 . . . . . . . . . . . 12 |- ( ( ( 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 } )
365363, 364syl 17 . . . . . . . . . . 11 |- ( 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 } )
366 eqeq2 2633 . . . . . . . . . . . 12 |- ( n = J -> ( sum_ t e. ( R u. { Z } ) ( c ` t ) = n <-> sum_ t e. ( R u. { Z } ) ( c ` t ) = J ) )
367366rabbidv 3189 . . . . . . . . . . 11 |- ( 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 } )
368365, 367eqtrd 2656 . . . . . . . . . 10 |- ( 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 } )
369368adantl 482 . . . . . . . . 9 |- ( ( 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 } )
370 ovex 6678 . . . . . . . . . . 11 |- ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. _V
371370rabex 4813 . . . . . . . . . 10 |- { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V
372371a1i 11 . . . . . . . . 9 |- ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. _V )
373361, 369, 45, 372fvmptd 6288 . . . . . . . 8 |- ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) = { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } )
374 fzfid 12772 . . . . . . . . . 10 |- ( ph -> ( 0 ... J ) e. Fin )
375 snfi 8038 . . . . . . . . . . . 12 |- { Z } e. Fin
376375a1i 11 . . . . . . . . . . 11 |- ( ph -> { Z } e. Fin )
377 unfi 8227 . . . . . . . . . . 11 |- ( ( R e. Fin /\ { Z } e. Fin ) -> ( R u. { Z } ) e. Fin )
3786, 376, 377syl2anc 693 . . . . . . . . . 10 |- ( ph -> ( R u. { Z } ) e. Fin )
379 mapfi 8262 . . . . . . . . . 10 |- ( ( ( 0 ... J ) e. Fin /\ ( R u. { Z } ) e. Fin ) -> ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. Fin )
380374, 378, 379syl2anc 693 . . . . . . . . 9 |- ( ph -> ( ( 0 ... J ) ^m ( R u. { Z } ) ) e. Fin )
381 ssrab2 3687 . . . . . . . . . 10 |- { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } C_ ( ( 0 ... J ) ^m ( R u. { Z } ) )
382381a1i 11 . . . . . . . . 9 |- ( 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 } ) ) )
383 ssfi 8180 . . . . . . . . 9 |- ( ( ( ( 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 )
384380, 382, 383syl2anc 693 . . . . . . . 8 |- ( ph -> { c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) | sum_ t e. ( R u. { Z } ) ( c ` t ) = J } e. Fin )
385373, 384eqeltrd 2701 . . . . . . 7 |- ( ph -> ( ( C ` ( R u. { Z } ) ) ` J ) e. Fin )
386385adantr 481 . . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( C ` ( R u. { Z } ) ) ` J ) e. Fin )
387 dvnprodlem2.d . . . . . . . 8 |- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
38848, 45, 387, 3, 23, 10, 354dvnprodlem1 40161 . . . . . . 7 |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
389388adantr 481 . . . . . 6 |- ( ( ph /\ x e. X ) -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
390 simpr 477 . . . . . . . 8 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
391 opex 4932 . . . . . . . . 9 |- <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V
392391a1i 11 . . . . . . . 8 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V )
393387fvmpt2 6291 . . . . . . . 8 |- ( ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) /\ <. ( J - ( c ` Z ) ) , ( c |` R ) >. e. _V ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
394390, 392, 393syl2anc 693 . . . . . . 7 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
395394adantlr 751 . . . . . 6 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( D ` c ) = <. ( J - ( c ` Z ) ) , ( c |` R ) >. )
39645adantr 481 . . . . . . . . . 10 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> J e. NN0 )
397 eliun 4524 . . . . . . . . . . . . . 14 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) <-> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
398397biimpi 206 . . . . . . . . . . . . 13 |- ( p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) -> E. k e. ( 0 ... J ) p e. ( { k } X. ( ( C ` R ) ` k ) ) )
399398adantl 482 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
400 nfv 1843 . . . . . . . . . . . . . 14 |- F/ k ph
401 nfcv 2764 . . . . . . . . . . . . . . 15 |- F/_ k p
402 nfiu1 4550 . . . . . . . . . . . . . . 15 |- F/_ k U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
403401, 402nfel 2777 . . . . . . . . . . . . . 14 |- F/ k p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) )
404400, 403nfan 1828 . . . . . . . . . . . . 13 |- F/ k ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
405 nfv 1843 . . . . . . . . . . . . 13 |- F/ k ( 1st ` p ) e. ( 0 ... J )
406 xp1st 7198 . . . . . . . . . . . . . . . . . 18 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. { k } )
407 elsni 4194 . . . . . . . . . . . . . . . . . 18 |- ( ( 1st ` p ) e. { k } -> ( 1st ` p ) = k )
408406, 407syl 17 . . . . . . . . . . . . . . . . 17 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) = k )
409408adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) = k )
410 simpl 473 . . . . . . . . . . . . . . . 16 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> k e. ( 0 ... J ) )
411409, 410eqeltrd 2701 . . . . . . . . . . . . . . 15 |- ( ( k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
412411ex 450 . . . . . . . . . . . . . 14 |- ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 1st ` p ) e. ( 0 ... J ) ) )
413412a1i 11 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
414404, 405, 413rexlimd 3026 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
415399, 414mpd 15 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
416 elfzelz 12342 . . . . . . . . . . 11 |- ( ( 1st ` p ) e. ( 0 ... J ) -> ( 1st ` p ) e. ZZ )
417415, 416syl 17 . . . . . . . . . 10 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ZZ )
418396, 417bccld 39531 . . . . . . . . 9 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J _C ( 1st ` p ) ) e. NN0 )
419418nn0cnd 11353 . . . . . . . 8 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J _C ( 1st ` p ) ) e. CC )
420419adantlr 751 . . . . . . 7 |- ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J _C ( 1st ` p ) ) e. CC )
421 elfznn0 12433 . . . . . . . . . . . . . 14 |- ( ( 1st ` p ) e. ( 0 ... J ) -> ( 1st ` p ) e. NN0 )
422415, 421syl 17 . . . . . . . . . . . . 13 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. NN0 )
423422faccld 13071 . . . . . . . . . . . 12 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ! ` ( 1st ` p ) ) e. NN )
424423nncnd 11036 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ! ` ( 1st ` p ) ) e. CC )
425424adantlr 751 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ! ` ( 1st ` p ) ) e. CC )
4266adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> R e. Fin )
427 nfv 1843 . . . . . . . . . . . . . . . 16 |- F/ k ( 2nd ` p ) : R --> ( 0 ... J )
42886, 84eqsstrd 3639 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) C_ ( ( 0 ... k ) ^m R ) )
429 ovex 6678 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 ... J ) e. _V
430429a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( 0 ... J ) -> ( 0 ... J ) e. _V )
431 mapss 7900 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 0 ... J ) e. _V /\ ( 0 ... k ) C_ ( 0 ... J ) ) -> ( ( 0 ... k ) ^m R ) C_ ( ( 0 ... J ) ^m R ) )
432430, 124, 431syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... J ) -> ( ( 0 ... k ) ^m R ) C_ ( ( 0 ... J ) ^m R ) )
433432adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( 0 ... k ) ^m R ) C_ ( ( 0 ... J ) ^m R ) )
434428, 433sstrd 3613 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... J ) ) -> ( ( C ` R ) ` k ) C_ ( ( 0 ... J ) ^m R ) )
4354343adant3 1081 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( C ` R ) ` k ) C_ ( ( 0 ... J ) ^m R ) )
436 xp2nd 7199 . . . . . . . . . . . . . . . . . . . . 21 |- ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
4374363ad2ant3 1084 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( C ` R ) ` k ) )
438435, 437sseldd 3604 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) e. ( ( 0 ... J ) ^m R ) )
439 elmapi 7879 . . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` p ) e. ( ( 0 ... J ) ^m R ) -> ( 2nd ` p ) : R --> ( 0 ... J ) )
440438, 439syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) : R --> ( 0 ... J ) )
4414403exp 1264 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( 2nd ` p ) : R --> ( 0 ... J ) ) ) )
442441adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
443404, 427, 442rexlimd 3026 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
444399, 443mpd 15 . . . . . . . . . . . . . 14 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 2nd ` p ) : R --> ( 0 ... J ) )
445444ffvelrnda 6359 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... J ) )
446 elfznn0 12433 . . . . . . . . . . . . . . 15 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... J ) -> ( ( 2nd ` p ) ` t ) e. NN0 )
447446faccld 13071 . . . . . . . . . . . . . 14 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... J ) -> ( ! ` ( ( 2nd ` p ) ` t ) ) e. NN )
448447nncnd 11036 . . . . . . . . . . . . 13 |- ( ( ( 2nd ` p ) ` t ) e. ( 0 ... J ) -> ( ! ` ( ( 2nd ` p ) ` t ) ) e. CC )
449445, 448syl 17 . . . . . . . . . . . 12 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ! ` ( ( 2nd ` p ) ` t ) ) e. CC )
450426, 449fprodcl 14682 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) e. CC )
451450adantlr 751 . . . . . . . . . 10 |- ( ( ( 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 )
452445, 447syl 17 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ! ` ( ( 2nd ` p ) ` t ) ) e. NN )
453 nnne0 11053 . . . . . . . . . . . . 13 |- ( ( ! ` ( ( 2nd ` p ) ` t ) ) e. NN -> ( ! ` ( ( 2nd ` p ) ` t ) ) =/= 0 )
454452, 453syl 17 . . . . . . . . . . . 12 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ! ` ( ( 2nd ` p ) ` t ) ) =/= 0 )
455426, 449, 454fprodn0 14709 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) =/= 0 )
456455adantlr 751 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> prod_ t e. R ( ! ` ( ( 2nd ` p ) ` t ) ) =/= 0 )
457425, 451, 456divcld 10801 . . . . . . . . 9 |- ( ( ( 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 )
4587adantr 481 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> R e. Fin )
459 simpll 790 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ph )
460459, 13sylancom 701 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> t e. T )
461459, 135syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( 0 ... J ) C_ ( 0 ... N ) )
462461, 445sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> ( ( 2nd ` p ) ` t ) e. ( 0 ... N ) )
463459, 460, 4623jca 1242 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
464 eleq1 2689 . . . . . . . . . . . . . . . 16 |- ( j = ( ( 2nd ` p ) ` t ) -> ( j e. ( 0 ... N ) <-> ( ( 2nd ` p ) ` t ) e. ( 0 ... N ) ) )
4654643anbi3d 1405 . . . . . . . . . . . . . . 15 |- ( j = ( ( 2nd ` p ) ` t ) -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ ( ( 2nd ` p ) ` t ) e. ( 0 ... N ) ) ) )
466 fveq2 6191 . . . . . . . . . . . . . . . 16 |- ( j = ( ( 2nd ` p ) ` t ) -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) )
467466feq1d 6030 . . . . . . . . . . . . . . 15 |- ( j = ( ( 2nd ` p ) ` t ) -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` ( ( 2nd ` p ) ` t ) ) : X --> CC ) )
468465, 467imbi12d 334 . . . . . . . . . . . . . 14 |- ( 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 ) ) )
469468, 147vtoclg 3266 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
470445, 463, 469sylc 65 . . . . . . . . . . . 12 |- ( ( ( 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 )
471470adantllr 755 . . . . . . . . . . 11 |- ( ( ( ( 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 )
47217adantlr 751 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) /\ t e. R ) -> x e. X )
473471, 472ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ( 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 )
474458, 473fprodcl 14682 . . . . . . . . 9 |- ( ( ( 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 )
475457, 474mulcld 10060 . . . . . . . 8 |- ( ( ( 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 )
476 nfv 1843 . . . . . . . . . . . . 13 |- F/ k ( J - ( 1st ` p ) ) e. ( 0 ... J )
477 simp1 1061 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ph )
4784113adant1 1079 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 1st ` p ) e. ( 0 ... J ) )
479 fznn0sub2 12446 . . . . . . . . . . . . . . . . 17 |- ( ( 1st ` p ) e. ( 0 ... J ) -> ( J - ( 1st ` p ) ) e. ( 0 ... J ) )
480479adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( 1st ` p ) e. ( 0 ... J ) ) -> ( J - ( 1st ` p ) ) e. ( 0 ... J ) )
481477, 478, 480syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... J ) /\ p e. ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ( 0 ... J ) )
4824813exp 1264 . . . . . . . . . . . . . 14 |- ( ph -> ( k e. ( 0 ... J ) -> ( p e. ( { k } X. ( ( C ` R ) ` k ) ) -> ( J - ( 1st ` p ) ) e. ( 0 ... J ) ) ) )
483482adantr 481 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
484404, 476, 483rexlimd 3026 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
485399, 484mpd 15 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ( 0 ... J ) )
486 simpl 473 . . . . . . . . . . . 12 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ph )
487486, 23syl 17 . . . . . . . . . . . 12 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> Z e. T )
488486, 135syl 17 . . . . . . . . . . . . 13 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( 0 ... J ) C_ ( 0 ... N ) )
489488, 485sseldd 3604 . . . . . . . . . . . 12 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( J - ( 1st ` p ) ) e. ( 0 ... N ) )
490486, 487, 4893jca 1242 . . . . . . . . . . 11 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ph /\ Z e. T /\ ( J - ( 1st ` p ) ) e. ( 0 ... N ) ) )
491 eleq1 2689 . . . . . . . . . . . . . 14 |- ( j = ( J - ( 1st ` p ) ) -> ( j e. ( 0 ... N ) <-> ( J - ( 1st ` p ) ) e. ( 0 ... N ) ) )
4924913anbi3d 1405 . . . . . . . . . . . . 13 |- ( j = ( J - ( 1st ` p ) ) -> ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ Z e. T /\ ( J - ( 1st ` p ) ) e. ( 0 ... N ) ) ) )
493 fveq2 6191 . . . . . . . . . . . . . 14 |- ( j = ( J - ( 1st ` p ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) )
494493feq1d 6030 . . . . . . . . . . . . 13 |- ( j = ( J - ( 1st ` p ) ) -> ( ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) : X --> CC ) )
495492, 494imbi12d 334 . . . . . . . . . . . 12 |- ( 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 ) ) )
496 simp2 1062 . . . . . . . . . . . . 13 |- ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) -> Z e. T )
497 id 22 . . . . . . . . . . . . 13 |- ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) -> ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) )
498263anbi2d 1404 . . . . . . . . . . . . . . 15 |- ( t = Z -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) ) )
499185fveq1d 6193 . . . . . . . . . . . . . . . 16 |- ( t = Z -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` j ) )
500499feq1d 6030 . . . . . . . . . . . . . . 15 |- ( t = Z -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) )
501498, 500imbi12d 334 . . . . . . . . . . . . . 14 |- ( 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 ) ) )
502501, 147vtoclg 3266 . . . . . . . . . . . . 13 |- ( Z e. T -> ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC ) )
503496, 497, 502sylc 65 . . . . . . . . . . . 12 |- ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC )
504495, 503vtoclg 3266 . . . . . . . . . . 11 |- ( ( 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 ) )
505485, 490, 504sylc 65 . . . . . . . . . 10 |- ( ( ph /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - ( 1st ` p ) ) ) : X --> CC )
506505adantlr 751 . . . . . . . . 9 |- ( ( ( 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 )
50734adantr 481 . . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ p e. U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) ) -> x e. X )
508506, 507ffvelrnd 6360 . . . . . . . 8 |- ( ( ( 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 )
509475, 508mulcld 10060 . . . . . . 7 |- ( ( ( 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 )
510420, 509mulcld 10060 . . . . . 6 |- ( ( ( 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 )
511342, 386, 389, 395, 510fsumf1o 14454 . . . . 5 |- ( ( 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 ) ) ) )
512 simpl 473 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ph )
513373adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( 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 } )
514390, 513eleqtrd 2703 . . . . . . . . . . . . . . 15 |- ( ( 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 } )
515381sseli 3599 . . . . . . . . . . . . . . 15 |- ( 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 } ) ) )
516514, 515syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) )
517 elmapi 7879 . . . . . . . . . . . . . 14 |- ( c e. ( ( 0 ... J ) ^m ( R u. { Z } ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
518516, 517syl 17 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
519 snidg 4206 . . . . . . . . . . . . . . . 16 |- ( Z e. T -> Z e. { Z } )
52023, 519syl 17 . . . . . . . . . . . . . . 15 |- ( ph -> Z e. { Z } )
521 elun2 3781 . . . . . . . . . . . . . . 15 |- ( Z e. { Z } -> Z e. ( R u. { Z } ) )
522520, 521syl 17 . . . . . . . . . . . . . 14 |- ( ph -> Z e. ( R u. { Z } ) )
523522adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. ( R u. { Z } ) )
524518, 523ffvelrnd 6360 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... J ) )
525 0zd 11389 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> 0 e. ZZ )
526126adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> J e. ZZ )
527 fzssz 12343 . . . . . . . . . . . . . . . . . 18 |- ( 0 ... J ) C_ ZZ
528527sseli 3599 . . . . . . . . . . . . . . . . 17 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) e. ZZ )
529528adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( c ` Z ) e. ZZ )
530526, 529zsubcld 11487 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( J - ( c ` Z ) ) e. ZZ )
531525, 526, 5303jca 1242 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) )
532 elfzle2 12345 . . . . . . . . . . . . . . . 16 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) <_ J )
533532adantl 482 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( c ` Z ) <_ J )
534167adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> J e. RR )
535529zred 11482 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( c ` Z ) e. RR )
536534, 535subge0d 10617 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( 0 <_ ( J - ( c ` Z ) ) <-> ( c ` Z ) <_ J ) )
537533, 536mpbird 247 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> 0 <_ ( J - ( c ` Z ) ) )
538 elfzle1 12344 . . . . . . . . . . . . . . . 16 |- ( ( c ` Z ) e. ( 0 ... J ) -> 0 <_ ( c ` Z ) )
539538adantl 482 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> 0 <_ ( c ` Z ) )
540534, 535subge02d 10619 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( 0 <_ ( c ` Z ) <-> ( J - ( c ` Z ) ) <_ J ) )
541539, 540mpbid 222 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( J - ( c ` Z ) ) <_ J )
542531, 537, 541jca32 558 . . . . . . . . . . . . 13 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) /\ ( 0 <_ ( J - ( c ` Z ) ) /\ ( J - ( c ` Z ) ) <_ J ) ) )
543 elfz2 12333 . . . . . . . . . . . . 13 |- ( ( J - ( c ` Z ) ) e. ( 0 ... J ) <-> ( ( 0 e. ZZ /\ J e. ZZ /\ ( J - ( c ` Z ) ) e. ZZ ) /\ ( 0 <_ ( J - ( c ` Z ) ) /\ ( J - ( c ` Z ) ) <_ J ) ) )
544542, 543sylibr 224 . . . . . . . . . . . 12 |- ( ( ph /\ ( c ` Z ) e. ( 0 ... J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
545512, 524, 544syl2anc 693 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. ( 0 ... J ) )
546 bcval2 13092 . . . . . . . . . . 11 |- ( ( J - ( c ` Z ) ) e. ( 0 ... J ) -> ( J _C ( J - ( c ` Z ) ) ) = ( ( ! ` J ) / ( ( ! ` ( J - ( J - ( c ` Z ) ) ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) )
547545, 546syl 17 . . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J _C ( J - ( c ` Z ) ) ) = ( ( ! ` J ) / ( ( ! ` ( J - ( J - ( c ` Z ) ) ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) )
548167recnd 10068 . . . . . . . . . . . . . . 15 |- ( ph -> J e. CC )
549548adantr 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> J e. CC )
550 zsscn 11385 . . . . . . . . . . . . . . . . 17 |- ZZ C_ CC
551527, 550sstri 3612 . . . . . . . . . . . . . . . 16 |- ( 0 ... J ) C_ CC
552551a1i 11 . . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... J ) C_ CC )
553552, 524sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. CC )
554549, 553nncand 10397 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( J - ( c ` Z ) ) ) = ( c ` Z ) )
555554fveq2d 6195 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( J - ( c ` Z ) ) ) ) = ( ! ` ( c ` Z ) ) )
556555oveq1d 6665 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ! ` ( J - ( J - ( c ` Z ) ) ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) = ( ( ! ` ( c ` Z ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) )
557556oveq2d 6666 . . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ! ` J ) / ( ( ! ` ( J - ( J - ( c ` Z ) ) ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) = ( ( ! ` J ) / ( ( ! ` ( c ` Z ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) )
55845faccld 13071 . . . . . . . . . . . . . 14 |- ( ph -> ( ! ` J ) e. NN )
559558nncnd 11036 . . . . . . . . . . . . 13 |- ( ph -> ( ! ` J ) e. CC )
560559adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` J ) e. CC )
561 elfznn0 12433 . . . . . . . . . . . . . . 15 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( c ` Z ) e. NN0 )
562524, 561syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. NN0 )
563562faccld 13071 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( c ` Z ) ) e. NN )
564563nncnd 11036 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( c ` Z ) ) e. CC )
565 elfznn0 12433 . . . . . . . . . . . . . . 15 |- ( ( J - ( c ` Z ) ) e. ( 0 ... J ) -> ( J - ( c ` Z ) ) e. NN0 )
566545, 565syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J - ( c ` Z ) ) e. NN0 )
567566faccld 13071 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( c ` Z ) ) ) e. NN )
568567nncnd 11036 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( c ` Z ) ) ) e. CC )
569563nnne0d 11065 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( c ` Z ) ) =/= 0 )
570567nnne0d 11065 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( c ` Z ) ) ) =/= 0 )
571560, 564, 568, 569, 570divdiv1d 10832 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ( ! ` J ) / ( ! ` ( c ` Z ) ) ) / ( ! ` ( J - ( c ` Z ) ) ) ) = ( ( ! ` J ) / ( ( ! ` ( c ` Z ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) )
572571eqcomd 2628 . . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ! ` J ) / ( ( ! ` ( c ` Z ) ) x. ( ! ` ( J - ( c ` Z ) ) ) ) ) = ( ( ( ! ` J ) / ( ! ` ( c ` Z ) ) ) / ( ! ` ( J - ( c ` Z ) ) ) ) )
573547, 557, 5723eqtrd 2660 . . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J _C ( J - ( c ` Z ) ) ) = ( ( ( ! ` J ) / ( ! ` ( c ` Z ) ) ) / ( ! ` ( J - ( c ` Z ) ) ) ) )
574573adantlr 751 . . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( J _C ( J - ( c ` Z ) ) ) = ( ( ( ! ` J ) / ( ! ` ( c ` Z ) ) ) / ( ! ` ( J - ( c ` Z ) ) ) ) )
575 fvres 6207 . . . . . . . . . . . . . . . . 17 |- ( t e. R -> ( ( c |` R ) ` t ) = ( c ` t ) )
576575fveq2d 6195 . . . . . . . . . . . . . . . 16 |- ( t e. R -> ( ! ` ( ( c |` R ) ` t ) ) = ( ! ` ( c ` t ) ) )
577576prodeq2i 14649 . . . . . . . . . . . . . . 15 |- prod_ t e. R ( ! ` ( ( c |` R ) ` t ) ) = prod_ t e. R ( ! ` ( c ` t ) )
578577oveq2i 6661 . . . . . . . . . . . . . 14 |- ( ( ! ` ( J - ( c ` Z ) ) ) / prod_ t e. R ( ! ` ( ( c |` R ) ` t ) ) ) = ( ( ! ` ( J - ( c ` Z ) ) ) / prod_ t e. R ( ! ` ( c ` t ) ) )
579575fveq2d 6195 . . . . . . . . . . . . . . . 16 |- ( t e. R -> ( ( S Dn ( H ` t ) ) ` ( ( c |` R ) ` t ) ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
580579fveq1d 6193 . . . . . . . . . . . . . . 15 |- ( t e. R -> ( ( ( S Dn ( H ` t ) ) ` ( ( c |` R ) ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
581580prodeq2i 14649 . . . . . . . . . . . . . 14 |- prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( ( c |` R ) ` t ) ) ` x ) = prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x )
582578, 581oveq12i 6662 . . . . . . . . . . . . 13 |- ( ( ( ! ` ( 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 ) )
583582a1i 11 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
584583adantlr 751 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
585568adantlr 751 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( c ` Z ) ) ) e. CC )
586512, 6syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
58777ssriv 3607 . . . . . . . . . . . . . . . . . 18 |- ( 0 ... J ) C_ NN0
588587a1i 11 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( 0 ... J ) C_ NN0 )
589518adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> c : ( R u. { Z } ) --> ( 0 ... J ) )
590 elun1 3780 . . . . . . . . . . . . . . . . . . 19 |- ( t e. R -> t e. ( R u. { Z } ) )
591590adantl 482 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. ( R u. { Z } ) )
592589, 591ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... J ) )
593588, 592sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. NN0 )
594593faccld 13071 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. NN )
595594nncnd 11036 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ! ` ( c ` t ) ) e. CC )
596586, 595fprodcl 14682 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. CC )
597596adantlr 751 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. CC )
5987adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> R e. Fin )
599512adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ph )
600512, 13sylan 488 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> t e. T )
601599, 135syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( 0 ... J ) C_ ( 0 ... N ) )
602601, 592sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( c ` t ) e. ( 0 ... N ) )
603599, 600, 602, 148syl3anc 1326 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
604603adantllr 755 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
60517adantlr 751 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> x e. X )
606604, 605ffvelrnd 6360 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. R ) -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
607598, 606fprodcl 14682 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) e. CC )
608586, 594fprodnncl 14685 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) e. NN )
609 nnne0 11053 . . . . . . . . . . . . . 14 |- ( prod_ t e. R ( ! ` ( c ` t ) ) e. NN -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
610608, 609syl 17 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
611610adantlr 751 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. R ( ! ` ( c ` t ) ) =/= 0 )
612585, 597, 607, 611div32d 10824 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) )
613584, 612eqtrd 2656 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
614554fveq2d 6195 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( J - ( J - ( c ` Z ) ) ) ) = ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) )
615614fveq1d 6193 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( J - ( J - ( c ` Z ) ) ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) ` x ) )
616615adantlr 751 . . . . . . . . . 10 |- ( ( ( 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 ) )
617613, 616oveq12d 6668 . . . . . . . . 9 |- ( ( ( 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 ) ) )
618607, 597, 611divcld 10801 . . . . . . . . . 10 |- ( ( ( 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 )
619512, 23syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
620512, 135syl 17 . . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( 0 ... J ) C_ ( 0 ... N ) )
621620, 524sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( c ` Z ) e. ( 0 ... N ) )
622512, 619, 6213jca 1242 . . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ph /\ Z e. T /\ ( c ` Z ) e. ( 0 ... N ) ) )
623 eleq1 2689 . . . . . . . . . . . . . . . 16 |- ( j = ( c ` Z ) -> ( j e. ( 0 ... N ) <-> ( c ` Z ) e. ( 0 ... N ) ) )
6246233anbi3d 1405 . . . . . . . . . . . . . . 15 |- ( j = ( c ` Z ) -> ( ( ph /\ Z e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ Z e. T /\ ( c ` Z ) e. ( 0 ... N ) ) ) )
625 fveq2 6191 . . . . . . . . . . . . . . . 16 |- ( j = ( c ` Z ) -> ( ( S Dn ( H ` Z ) ) ` j ) = ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) )
626625feq1d 6030 . . . . . . . . . . . . . . 15 |- ( j = ( c ` Z ) -> ( ( ( S Dn ( H ` Z ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) : X --> CC ) )
627624, 626imbi12d 334 . . . . . . . . . . . . . 14 |- ( 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 ) ) )
628627, 503vtoclg 3266 . . . . . . . . . . . . 13 |- ( ( c ` Z ) e. ( 0 ... J ) -> ( ( ph /\ Z e. T /\ ( c ` Z ) e. ( 0 ... N ) ) -> ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) : X --> CC ) )
629524, 622, 628sylc 65 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) : X --> CC )
630629adantlr 751 . . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) : X --> CC )
63134adantr 481 . . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> x e. X )
632630, 631ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) ` x ) e. CC )
633585, 618, 632mulassd 10063 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
634617, 633eqtrd 2656 . . . . . . . 8 |- ( ( ( 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 ) ) ) )
635574, 634oveq12d 6668 . . . . . . 7 |- ( ( ( 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 ) ) ) ) )
636559ad2antrr 762 . . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` J ) e. CC )
637564adantlr 751 . . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( c ` Z ) ) e. CC )
638569adantlr 751 . . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( c ` Z ) ) =/= 0 )
639636, 637, 638divcld 10801 . . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ( ! ` J ) / ( ! ` ( c ` Z ) ) ) e. CC )
640618, 632mulcld 10060 . . . . . . . 8 |- ( ( ( 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 )
641570adantlr 751 . . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( ! ` ( J - ( c ` Z ) ) ) =/= 0 )
642639, 585, 640, 641dmmcand 39528 . . . . . . 7 |- ( ( ( 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 ) ) ) )
643607, 632, 597, 611div23d 10838 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
644643eqcomd 2628 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
645 nfv 1843 . . . . . . . . . . . . 13 |- F/ t ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
646 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ t ( ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) ` x )
647619adantlr 751 . . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> Z e. T )
64811adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
649 fveq2 6191 . . . . . . . . . . . . . . 15 |- ( t = Z -> ( c ` t ) = ( c ` Z ) )
650185, 649fveq12d 6197 . . . . . . . . . . . . . 14 |- ( t = Z -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) = ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) )
651650fveq1d 6193 . . . . . . . . . . . . 13 |- ( t = Z -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = ( ( ( S Dn ( H ` Z ) ) ` ( c ` Z ) ) ` x ) )
652645, 646, 598, 647, 648, 606, 651, 632fprodsplitsn 14720 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
653652eqcomd 2628 . . . . . . . . . . 11 |- ( ( ( 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 ) )
654653oveq1d 6665 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
655644, 654eqtrd 2656 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
656655oveq2d 6666 . . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
657598, 375, 377sylancl 694 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( R u. { Z } ) e. Fin )
658512adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ph )
659354sselda 3603 . . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( R u. { Z } ) ) -> t e. T )
660659adantlr 751 . . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> t e. T )
661518, 620fssd 6057 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> c : ( R u. { Z } ) --> ( 0 ... N ) )
662661ffvelrnda 6359 . . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( c ` t ) e. ( 0 ... N ) )
663658, 660, 662, 148syl3anc 1326 . . . . . . . . . . . 12 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
664663adantllr 755 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) : X --> CC )
665631adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> x e. X )
666664, 665ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ( 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 )
667657, 666fprodcl 14682 . . . . . . . . 9 |- ( ( ( 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 )
668636, 637, 667, 597, 638, 611divmuldivd 10842 . . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
669564, 596mulcomd 10061 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
670 nfv 1843 . . . . . . . . . . . . . 14 |- F/ t ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) )
671 nfcv 2764 . . . . . . . . . . . . . 14 |- F/_ t ( ! ` ( c ` Z ) )
672512, 10syl 17 . . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> -. Z e. R )
673649fveq2d 6195 . . . . . . . . . . . . . 14 |- ( t = Z -> ( ! ` ( c ` t ) ) = ( ! ` ( c ` Z ) ) )
674670, 671, 586, 619, 672, 595, 673, 564fprodsplitsn 14720 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
675674eqcomd 2628 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
676669, 675eqtrd 2656 . . . . . . . . . . 11 |- ( ( 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 ) ) )
677676oveq2d 6666 . . . . . . . . . 10 |- ( ( 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 ) ) ) )
678677adantlr 751 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
679512, 378syl 17 . . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> ( R u. { Z } ) e. Fin )
680587a1i 11 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( 0 ... J ) C_ NN0 )
681518ffvelrnda 6359 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( c ` t ) e. ( 0 ... J ) )
682680, 681sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( c ` t ) e. NN0 )
683682faccld 13071 . . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ! ` ( c ` t ) ) e. NN )
684683nncnd 11036 . . . . . . . . . . . 12 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ! ` ( c ` t ) ) e. CC )
685679, 684fprodcl 14682 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) e. CC )
686685adantlr 751 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) e. CC )
687683nnne0d 11065 . . . . . . . . . . . 12 |- ( ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) /\ t e. ( R u. { Z } ) ) -> ( ! ` ( c ` t ) ) =/= 0 )
688679, 684, 687fprodn0 14709 . . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) =/= 0 )
689688adantlr 751 . . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ) -> prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) =/= 0 )
690636, 667, 686, 689div23d 10838 . . . . . . . . 9 |- ( ( ( 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 ) ) )
691 eqidd 2623 . . . . . . . . 9 |- ( ( ( 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 ) ) )
692678, 690, 6913eqtrd 2660 . . . . . . . 8 |- ( ( ( 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 ) ) )
693656, 668, 6923eqtrd 2660 . . . . . . 7 |- ( ( ( 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 ) ) )
694635, 642, 6933eqtrd 2660 . . . . . 6 |- ( ( ( 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 ) ) )
695694sumeq2dv 14433 . . . . 5 |- ( ( 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 ) ) )
696511, 695eqtrd 2656 . . . 4 |- ( ( 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 ) ) )
697299, 323, 6963eqtrd 2660 . . 3 |- ( ( 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 ) ) )
698697mpteq2dva 4744 . 2 |- ( 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 ) ) ) )
69939, 215, 6983eqtrd 2660 1 |- ( 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 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   ~Pcpw 4158   {csn 4177   {cpr 4179   <.cop 4183   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   |` cres 5116   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   x. cmul 9941   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   !cfa 13060   _C cbc 13089   sum_csu 14416   prod_cprod 14635   ↾t crest 16081   TopOpenctopn 16082  ℂfldccnfld 19746   Dncdvn 23628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-prod 14636  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631  df-dvn 23632
This theorem is referenced by:  dvnprodlem3  40163
  Copyright terms: Public domain W3C validator