Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem2 Structured version   Unicode version

Theorem dvnprodlem2 37648
Description: Induction step for dvnprodlem2 37648. (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:    C, c,
k, t    D, c,
t    H, c, j, k, t    x, H, c, k, 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 1752 . . . . . 6  |-  F/ t ( ph  /\  x  e.  X )
2 nfcv 2585 . . . . . 6  |-  F/_ t
( ( H `  Z ) `  x
)
3 dvnprodlem2.t . . . . . . . 8  |-  ( ph  ->  T  e.  Fin )
4 dvnprodlem2.r . . . . . . . 8  |-  ( ph  ->  R  C_  T )
5 ssfi 7796 . . . . . . . 8  |-  ( ( T  e.  Fin  /\  R  C_  T )  ->  R  e.  Fin )
63, 4, 5syl2anc 666 . . . . . . 7  |-  ( ph  ->  R  e.  Fin )
76adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  R  e.  Fin )
8 dvnprodlem2.z . . . . . . 7  |-  ( ph  ->  Z  e.  ( T 
\  R ) )
98adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  Z  e.  ( T  \  R
) )
108eldifbd 3450 . . . . . . 7  |-  ( ph  ->  -.  Z  e.  R
)
1110adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  -.  Z  e.  R )
12 simpl 459 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  R )  ->  ph )
134sselda 3465 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  R )  ->  t  e.  T )
14 dvnprodlem2.h . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  ( H `  t ) : X --> CC )
1512, 13, 14syl2anc 666 . . . . . . . 8  |-  ( (
ph  /\  t  e.  R )  ->  ( H `  t ) : X --> CC )
1615adantlr 720 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  ( H `  t ) : X --> CC )
17 simplr 761 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  x  e.  X )
1816, 17ffvelrnd 6036 . . . . . 6  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  (
( H `  t
) `  x )  e.  CC )
19 fveq2 5879 . . . . . . 7  |-  ( t  =  Z  ->  ( H `  t )  =  ( H `  Z ) )
2019fveq1d 5881 . . . . . 6  |-  ( t  =  Z  ->  (
( H `  t
) `  x )  =  ( ( H `
 Z ) `  x ) )
21 id 23 . . . . . . . . 9  |-  ( ph  ->  ph )
22 eldifi 3588 . . . . . . . . . 10  |-  ( Z  e.  ( T  \  R )  ->  Z  e.  T )
238, 22syl 17 . . . . . . . . 9  |-  ( ph  ->  Z  e.  T )
24 simpr 463 . . . . . . . . . 10  |-  ( (
ph  /\  Z  e.  T )  ->  Z  e.  T )
25 id 23 . . . . . . . . . 10  |-  ( (
ph  /\  Z  e.  T )  ->  ( ph  /\  Z  e.  T
) )
26 eleq1 2495 . . . . . . . . . . . . 13  |-  ( t  =  Z  ->  (
t  e.  T  <->  Z  e.  T ) )
2726anbi2d 709 . . . . . . . . . . . 12  |-  ( t  =  Z  ->  (
( ph  /\  t  e.  T )  <->  ( ph  /\  Z  e.  T ) ) )
2819feq1d 5730 . . . . . . . . . . . 12  |-  ( t  =  Z  ->  (
( H `  t
) : X --> CC  <->  ( H `  Z ) : X --> CC ) )
2927, 28imbi12d 322 . . . . . . . . . . 11  |-  ( t  =  Z  ->  (
( ( ph  /\  t  e.  T )  ->  ( H `  t
) : X --> CC )  <-> 
( ( ph  /\  Z  e.  T )  ->  ( H `  Z
) : X --> CC ) ) )
3029, 14vtoclg 3140 . . . . . . . . . 10  |-  ( Z  e.  T  ->  (
( ph  /\  Z  e.  T )  ->  ( H `  Z ) : X --> CC ) )
3124, 25, 30sylc 63 . . . . . . . . 9  |-  ( (
ph  /\  Z  e.  T )  ->  ( H `  Z ) : X --> CC )
3221, 23, 31syl2anc 666 . . . . . . . 8  |-  ( ph  ->  ( H `  Z
) : X --> CC )
3332adantr 467 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  ( H `  Z ) : X --> CC )
34 simpr 463 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  X )
3533, 34ffvelrnd 6036 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  (
( H `  Z
) `  x )  e.  CC )
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 14036 . . . . 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 4508 . . . 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 6319 . . 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 5881 . 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 14039 . . 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 11889 . . . 4  |-  ( J  e.  ( 0 ... N )  ->  J  e.  NN0 )
4543, 44syl 17 . . 3  |-  ( ph  ->  J  e.  NN0 )
46 eqid 2423 . . 3  |-  ( x  e.  X  |->  prod_ t  e.  R  ( ( H `  t ) `  x ) )  =  ( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
47 eqid 2423 . . 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 6311 . . . . . . . . . . . . . 14  |-  ( s  =  R  ->  (
( 0 ... n
)  ^m  s )  =  ( ( 0 ... n )  ^m  R ) )
51 rabeq 3075 . . . . . . . . . . . . . 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 13748 . . . . . . . . . . . . . . 15  |-  ( s  =  R  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  R  (
c `  t )
)
5453eqeq1d 2425 . . . . . . . . . . . . . 14  |-  ( s  =  R  ->  ( sum_ t  e.  s  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  n ) )
5554rabbidv 3073 . . . . . . . . . . . . 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 2464 . . . . . . . . . . . 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 4509 . . . . . . . . . . 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 468 . . . . . . . . . 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 4568 . . . . . . . . . . . . . 14  |-  ( ( R  C_  T  /\  T  e.  Fin )  ->  R  e.  _V )
604, 3, 59syl2anc 666 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  _V )
61 elpwg 3988 . . . . . . . . . . . . 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 236 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  ~P T
)
6463adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  R  e.  ~P T )
65 nn0ex 10877 . . . . . . . . . . . 12  |-  NN0  e.  _V
6665mptex 6149 . . . . . . . . . . 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 5968 . . . . . . . . 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 6311 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
0 ... n )  =  ( 0 ... k
) )
7069oveq1d 6318 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( 0 ... n
)  ^m  R )  =  ( ( 0 ... k )  ^m  R ) )
71 rabeq 3075 . . . . . . . . . . . 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 2438 . . . . . . . . . . . 12  |-  ( n  =  k  ->  ( sum_ t  e.  R  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  k ) )
7473rabbidv 3073 . . . . . . . . . . 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 2464 . . . . . . . . . 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 468 . . . . . . . . 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 11889 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  e.  NN0 )
7877adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  NN0 )
79 fzfid 12187 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... k
)  e.  Fin )
80 mapfi 7874 . . . . . . . . . . . 12  |-  ( ( ( 0 ... k
)  e.  Fin  /\  R  e.  Fin )  ->  ( ( 0 ... k )  ^m  R
)  e.  Fin )
8179, 6, 80syl2anc 666 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 0 ... k )  ^m  R
)  e.  Fin )
8281adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0 ... k
)  ^m  R )  e.  Fin )
83 ssrab2 3547 . . . . . . . . . . 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 4569 . . . . . . . . 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 5968 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  =  { c  e.  ( ( 0 ... k
)  ^m  R )  |  sum_ t  e.  R  ( c `  t
)  =  k } )
87 ssfi 7796 . . . . . . . . . 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 667 . . . . . . . . 9  |-  ( ph  ->  { c  e.  ( ( 0 ... k
)  ^m  R )  |  sum_ t  e.  R  ( c `  t
)  =  k }  e.  Fin )
8988adantr 467 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  { c  e.  ( ( 0 ... k )  ^m  R )  |  sum_ t  e.  R  (
c `  t )  =  k }  e.  Fin )
9086, 89eqeltrd 2511 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  e.  Fin )
9190adantr 467 . . . . . 6  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  ->  (
( C `  R
) `  k )  e.  Fin )
9277faccld 37381 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... J )  ->  ( ! `  k )  e.  NN )
9392nncnd 10627 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  ( ! `  k )  e.  CC )
9493ad2antlr 732 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  ( ! `  k )  e.  CC )
956adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
9695adantlr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
97 elfznn0 11889 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( 0 ... k )  ->  z  e.  NN0 )
9897ssriv 3469 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  c  e.  ( ( C `  R ) `  k
) )
10186eleq2d 2493 . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . 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 3461 . . . . . . . . . . . . . . . . 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 7499 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  c : R --> ( 0 ... k ) )
109 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  t  e.  R )
110108, 109ffvelrnd 6036 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... k
) )
11199, 110sseldd 3466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  NN0 )
112111faccld 37381 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  e.  NN )
113112nncnd 10627 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  e.  CC )
11496, 113fprodcl 13999 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  prod_ t  e.  R  ( ! `
 ( c `  t ) )  e.  CC )
115112nnne0d 10656 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  =/=  0 )
11696, 113, 115fprodn0 14026 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  prod_ t  e.  R  ( ! `
 ( c `  t ) )  =/=  0 )
11794, 114, 116divcld 10385 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  (
( ! `  k
)  /  prod_ t  e.  R  ( ! `  ( c `  t
) ) )  e.  CC )
118117adantlr 720 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  ->  (
( ! `  k
)  /  prod_ t  e.  R  ( ! `  ( c `  t
) ) )  e.  CC )
11996adantlr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
12021ad4antr 737 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  ph )
121120, 13sylancom 672 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  t  e.  T )
122 elfzuz3 11799 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  J  e.  ( ZZ>= `  k )
)
123 fzss2 11840 . . . . . . . . . . . . . . . 16  |-  ( J  e.  ( ZZ>= `  k
)  ->  ( 0 ... k )  C_  ( 0 ... J
) )
124122, 123syl 17 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0 ... k )  C_  ( 0 ... J
) )
125124adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... k )  C_  ( 0 ... J
) )
12645nn0zd 11040 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  ZZ )
127 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  NN0 )
128127nn0zd 11040 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ZZ )
129 elfzle2 11805 . . . . . . . . . . . . . . . . . . 19  |-  ( J  e.  ( 0 ... N )  ->  J  <_  N )
13043, 129syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  <_  N )
131126, 128, 1303jca 1186 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( J  e.  ZZ  /\  N  e.  ZZ  /\  J  <_  N ) )
132 eluz2 11167 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  J
)  <->  ( J  e.  ZZ  /\  N  e.  ZZ  /\  J  <_  N ) )
133131, 132sylibr 216 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ( ZZ>= `  J ) )
134 fzss2 11840 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  J
)  ->  ( 0 ... J )  C_  ( 0 ... N
) )
135133, 134syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0 ... J
)  C_  ( 0 ... N ) )
136135adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... J )  C_  ( 0 ... N
) )
137125, 136sstrd 3475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... k )  C_  ( 0 ... N
) )
138137ad2antrr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
0 ... k )  C_  ( 0 ... N
) )
139138, 110sseldd 3466 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... N
) )
140139adantllr 724 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... N
) )
141 fvex 5889 . . . . . . . . . . 11  |-  ( c `
 t )  e. 
_V
142 eleq1 2495 . . . . . . . . . . . . 13  |-  ( j  =  ( c `  t )  ->  (
j  e.  ( 0 ... N )  <->  ( c `  t )  e.  ( 0 ... N ) ) )
1431423anbi3d 1342 . . . . . . . . . . . 12  |-  ( j  =  ( c `  t )  ->  (
( ph  /\  t  e.  T  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  T  /\  ( c `  t
)  e.  ( 0 ... N ) ) ) )
144 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  ( c `  t )  ->  (
( S  Dn
( H `  t
) ) `  j
)  =  ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) )
145144feq1d 5730 . . . . . . . . . . . 12  |-  ( j  =  ( c `  t )  ->  (
( ( S  Dn ( H `  t ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) : X --> CC ) )
146143, 145imbi12d 322 . . . . . . . . . . 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 3134 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T  /\  ( c `  t )  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) : X --> CC )
149120, 121, 140, 148syl3anc 1265 . . . . . . . . 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 768 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  x  e.  X )
151149, 150ffvelrnd 6036 . . . . . . . 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 13999 . . . . . . 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 9665 . . . . . 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 13792 . . . . 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 2423 . . . . 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 6059 . . . 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 467 . . . . . 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 10951 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  0  e.  ZZ )
160128adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  N  e.  ZZ )
161 elfzelz 11802 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  e.  ZZ )
162161adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  ZZ )
163159, 160, 1623jca 1186 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ ) )
164 elfzle1 11804 . . . . . . . . 9  |-  ( k  e.  ( 0 ... J )  ->  0  <_  k )
165164adantl 468 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  0  <_  k )
166162zred 11042 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  RR )
16745nn0red 10928 . . . . . . . . . 10  |-  ( ph  ->  J  e.  RR )
168167adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  J  e.  RR )
169160zred 11042 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  N  e.  RR )
170 elfzle2 11805 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  <_  J )
171170adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  <_  J )
172130adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  J  <_  N )
173166, 168, 169, 171, 172letrd 9794 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  <_  N )
174163, 165, 173jca32 538 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  ( 0  <_  k  /\  k  <_  N ) ) )
175 elfz2 11793 . . . . . . 7  |-  ( k  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  (
0  <_  k  /\  k  <_  N ) ) )
176174, 175sylibr 216 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  ( 0 ... N
) )
177 rspa 2793 . . . . . 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 666 . . . . 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 5730 . . . 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 236 . . 3  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) ) ) `  k ) : X --> CC )
18123adantr 467 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  Z  e.  T )
182 simpl 459 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ph )
183182, 181, 1763jca 1186 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( ph  /\  Z  e.  T  /\  k  e.  (
0 ... N ) ) )
184263anbi2d 1341 . . . . . . 7  |-  ( t  =  Z  ->  (
( ph  /\  t  e.  T  /\  k  e.  ( 0 ... N
) )  <->  ( ph  /\  Z  e.  T  /\  k  e.  ( 0 ... N ) ) ) )
18519oveq2d 6319 . . . . . . . . 9  |-  ( t  =  Z  ->  ( S  Dn ( H `
 t ) )  =  ( S  Dn ( H `  Z ) ) )
186185fveq1d 5881 . . . . . . . 8  |-  ( t  =  Z  ->  (
( S  Dn
( H `  t
) ) `  k
)  =  ( ( S  Dn ( H `  Z ) ) `  k ) )
187186feq1d 5730 . . . . . . 7  |-  ( t  =  Z  ->  (
( ( S  Dn ( H `  t ) ) `  k ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  k ) : X --> CC ) )
188184, 187imbi12d 322 . . . . . 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 2495 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  e.  ( 0 ... N )  <->  k  e.  ( 0 ... N
) ) )
1901893anbi3d 1342 . . . . . . . 8  |-  ( j  =  k  ->  (
( ph  /\  t  e.  T  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  T  /\  k  e.  ( 0 ... N ) ) ) )
191 fveq2 5879 . . . . . . . . 9  |-  ( j  =  k  ->  (
( S  Dn
( H `  t
) ) `  j
)  =  ( ( S  Dn ( H `  t ) ) `  k ) )
192191feq1d 5730 . . . . . . . 8  |-  ( j  =  k  ->  (
( ( S  Dn ( H `  t ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  t ) ) `  k ) : X --> CC ) )
193190, 192imbi12d 322 . . . . . . 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 2069 . . . . . 6  |-  ( (
ph  /\  t  e.  T  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `
 t ) ) `
 k ) : X --> CC )
195188, 194vtoclg 3140 . . . . 5  |-  ( Z  e.  T  ->  (
( ph  /\  Z  e.  T  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
( H `  Z
) ) `  k
) : X --> CC ) )
196181, 183, 195sylc 63 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  k
) : X --> CC )
19732feqmptd 5932 . . . . . . . . 9  |-  ( ph  ->  ( H `  Z
)  =  ( x  e.  X  |->  ( ( H `  Z ) `
 x ) ) )
198197eqcomd 2431 . . . . . . . 8  |-  ( ph  ->  ( x  e.  X  |->  ( ( H `  Z ) `  x
) )  =  ( H `  Z ) )
199198oveq2d 6319 . . . . . . 7  |-  ( ph  ->  ( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) )  =  ( S  Dn
( H `  Z
) ) )
200199fveq1d 5881 . . . . . 6  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( ( H `
 Z ) `  x ) ) ) `
 k )  =  ( ( S  Dn ( H `  Z ) ) `  k ) )
201200adantr 467 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) ) `  k )  =  ( ( S  Dn
( H `  Z
) ) `  k
) )
202201feq1d 5730 . . . 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 236 . . 3  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) ) `  k ) : X --> CC )
204 fveq2 5879 . . . . . . . 8  |-  ( y  =  x  ->  (
( H `  t
) `  y )  =  ( ( H `
 t ) `  x ) )
205204prodeq2ad 37498 . . . . . . 7  |-  ( y  =  x  ->  prod_ t  e.  R  ( ( H `  t ) `
 y )  = 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
206205cbvmptv 4514 . . . . . 6  |-  ( y  e.  X  |->  prod_ t  e.  R  ( ( H `  t ) `  y ) )  =  ( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
207206oveq2i 6314 . . . . 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 5880 . . . 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 4505 . . 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 5879 . . . . . . 7  |-  ( y  =  x  ->  (
( H `  Z
) `  y )  =  ( ( H `
 Z ) `  x ) )
211210cbvmptv 4514 . . . . . 6  |-  ( y  e.  X  |->  ( ( H `  Z ) `
 y ) )  =  ( x  e.  X  |->  ( ( H `
 Z ) `  x ) )
212211oveq2i 6314 . . . . 5  |-  ( S  Dn ( y  e.  X  |->  ( ( H `  Z ) `
 y ) ) )  =  ( S  Dn ( x  e.  X  |->  ( ( H `  Z ) `
 x ) ) )
213212fveq1i 5880 . . . 4  |-  ( ( S  Dn ( y  e.  X  |->  ( ( H `  Z
) `  y )
) ) `  k
)  =  ( ( S  Dn ( x  e.  X  |->  ( ( H `  Z
) `  x )
) ) `  k
)
214213mpteq2i 4505 . . 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 37644 . 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 2795 . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . 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 4508 . . . . . . . . . . . 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 6148 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 5973 . . . . . . . . . . 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 720 . . . . . . . . . 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 5881 . . . . . . . . 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 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  x  e.  X )
228154an32s 812 . . . . . . . . . 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 5971 . . . . . . . . . 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 666 . . . . . . . . 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 2464 . . . . . . . 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 5879 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) ) `  k )  =  ( ( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) ) `  j ) )
233232cbvmptv 4514 . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) )  =  ( S  Dn
( H `  Z
) ) )
236235fveq1d 5881 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( S  Dn ( y  e.  X  |->  ( ( H `
 Z ) `  y ) ) ) `
 j )  =  ( ( S  Dn ( H `  Z ) ) `  j ) )
237236mpteq2dv 4509 . . . . . . . . . . . . 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 2464 . . . . . . . . . . . 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 467 . . . . . . . . . . 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 5879 . . . . . . . . . . . 12  |-  ( j  =  ( J  -  k )  ->  (
( S  Dn
( H `  Z
) ) `  j
)  =  ( ( S  Dn ( H `  Z ) ) `  ( J  -  k ) ) )
241240adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  j  =  ( J  -  k ) )  -> 
( ( S  Dn ( H `  Z ) ) `  j )  =  ( ( S  Dn
( H `  Z
) ) `  ( J  -  k )
) )
242 0zd 10951 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  0  e.  ZZ )
243 elfzel2 11800 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  J  e.  ZZ )
244243, 161zsubcld 11047 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  ( J  -  k )  e.  ZZ )
245242, 243, 2443jca 1186 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  (
0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k )  e.  ZZ ) )
246243zred 11042 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  J  e.  RR )
24777nn0red 10928 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  k  e.  RR )
248246, 247subge0d 10205 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0  <_  ( J  -  k )  <->  k  <_  J ) )
249170, 248mpbird 236 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  0  <_  ( J  -  k
) )
250246, 247subge02d 10207 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0  <_  k  <->  ( J  -  k )  <_  J ) )
251164, 250mpbid 214 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  ( J  -  k )  <_  J )
252245, 249, 251jca32 538 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... J )  ->  (
( 0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( J  -  k
)  /\  ( J  -  k )  <_  J ) ) )
253252adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( J  -  k
)  /\  ( J  -  k )  <_  J ) ) )
254 elfz2 11793 . . . . . . . . . . . 12  |-  ( ( J  -  k )  e.  ( 0 ... J )  <->  ( (
0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k )  e.  ZZ )  /\  (
0  <_  ( J  -  k )  /\  ( J  -  k
)  <_  J )
) )
255253, 254sylibr 216 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  -  k )  e.  ( 0 ... J
) )
256 fvex 5889 . . . . . . . . . . . 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 5968 . . . . . . . . . 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 720 . . . . . . . . 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 5881 . . . . . . . 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 6321 . . . . . . 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 6319 . . . . . 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 720 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  e.  Fin )
264 ovex 6331 . . . . . . . . . . . 12  |-  ( J  -  k )  e. 
_V
265 eleq1 2495 . . . . . . . . . . . . . 14  |-  ( j  =  ( J  -  k )  ->  (
j  e.  ( 0 ... J )  <->  ( J  -  k )  e.  ( 0 ... J
) ) )
266265anbi2d 709 . . . . . . . . . . . . 13  |-  ( j  =  ( J  -  k )  ->  (
( ph  /\  j  e.  ( 0 ... J
) )  <->  ( ph  /\  ( J  -  k
)  e.  ( 0 ... J ) ) ) )
267240feq1d 5730 . . . . . . . . . . . . 13  |-  ( j  =  ( J  -  k )  ->  (
( ( S  Dn ( H `  Z ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) : X --> CC ) )
268266, 267imbi12d 322 . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
k  e.  ( 0 ... J )  <->  j  e.  ( 0 ... J
) ) )
270269anbi2d 709 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ph  /\  k  e.  ( 0 ... J
) )  <->  ( ph  /\  j  e.  ( 0 ... J ) ) ) )
271 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( S  Dn
( H `  Z
) ) `  k
)  =  ( ( S  Dn ( H `  Z ) ) `  j ) )
272271feq1d 5730 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( S  Dn ( H `  Z ) ) `  k ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  j ) : X --> CC ) )
273270, 272imbi12d 322 . . . . . . . . . . . . 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 2069 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  j
) : X --> CC )
275264, 268, 274vtocl 3134 . . . . . . . . . . 11  |-  ( (
ph  /\  ( J  -  k )  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
276182, 255, 275syl2anc 666 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
277276adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
278277, 227ffvelrnd 6036 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) `  x
)  e.  CC )
279 anass 654 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  <->  ( ph  /\  ( k  e.  ( 0 ... J )  /\  x  e.  X
) ) )
280 ancom 452 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( 0 ... J )  /\  x  e.  X )  <->  ( x  e.  X  /\  k  e.  ( 0 ... J ) ) )
281280anbi2i 699 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  ( 0 ... J
)  /\  x  e.  X ) )  <->  ( ph  /\  ( x  e.  X  /\  k  e.  (
0 ... J ) ) ) )
282 anass 654 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  <->  ( ph  /\  ( x  e.  X  /\  k  e.  (
0 ... J ) ) ) )
283282bicomi 206 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  X  /\  k  e.  ( 0 ... J
) ) )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
284281, 283bitri 253 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  ( 0 ... J
)  /\  x  e.  X ) )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
285279, 284bitri 253 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
286285anbi1i 700 . . . . . . . . . 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 327 . . . . . . . . 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 212 . . . . . . . 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 13839 . . . . . . 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 6319 . . . . . 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 37385 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e. 
NN0 )
293292nn0cnd 10929 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e.  CC )
294293adantlr 720 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e.  CC )
295278adantr 467 . . . . . . . 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 9665 . . . . . . 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 13838 . . . . . 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 2468 . . . . 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 13762 . . . 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 3085 . . . . . . . 8  |-  k  e. 
_V
301 vex 3085 . . . . . . . 8  |-  c  e. 
_V
302300, 301op1std 6815 . . . . . . 7  |-  ( p  =  <. k ,  c
>.  ->  ( 1st `  p
)  =  k )
303302oveq2d 6319 . . . . . 6  |-  ( p  =  <. k ,  c
>.  ->  ( J  _C  ( 1st `  p ) )  =  ( J  _C  k ) )
304302fveq2d 5883 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( ! `  ( 1st `  p ) )  =  ( ! `
 k ) )
305300, 301op2ndd 6816 . . . . . . . . . . . 12  |-  ( p  =  <. k ,  c
>.  ->  ( 2nd `  p
)  =  c )
306305fveq1d 5881 . . . . . . . . . . 11  |-  ( p  =  <. k ,  c
>.  ->  ( ( 2nd `  p ) `  t
)  =  ( c `
 t ) )
307306fveq2d 5883 . . . . . . . . . 10  |-  ( p  =  <. k ,  c
>.  ->  ( ! `  ( ( 2nd `  p
) `  t )
)  =  ( ! `
 ( c `  t ) ) )
308307prodeq2ad 37498 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  prod_ t  e.  R  ( ! `  ( ( 2nd `  p ) `
 t ) )  =  prod_ t  e.  R  ( ! `  ( c `
 t ) ) )
309304, 308oveq12d 6321 . . . . . . . 8  |-  ( p  =  <. k ,  c
>.  ->  ( ( ! `
 ( 1st `  p
) )  /  prod_ t  e.  R  ( ! `
 ( ( 2nd `  p ) `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  R  ( ! `
 ( c `  t ) ) ) )
310306fveq2d 5883 . . . . . . . . . 10  |-  ( p  =  <. k ,  c
>.  ->  ( ( S  Dn ( H `
 t ) ) `
 ( ( 2nd `  p ) `  t
) )  =  ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) )
311310fveq1d 5881 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( ( ( S  Dn ( H `  t ) ) `  ( ( 2nd `  p ) `
 t ) ) `
 x )  =  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
312311prodeq2ad 37498 . . . . . . . 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 6321 . . . . . . 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 6319 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( J  -  ( 1st `  p ) )  =  ( J  -  k ) )
315314fveq2d 5883 . . . . . . . 8  |-  ( p  =  <. k ,  c
>.  ->  ( ( S  Dn ( H `
 Z ) ) `
 ( J  -  ( 1st `  p ) ) )  =  ( ( S  Dn
( H `  Z
) ) `  ( J  -  k )
) )
316315fveq1d 5881 . . . . . . 7  |-  ( p  =  <. k ,  c
>.  ->  ( ( ( S  Dn ( H `  Z ) ) `  ( J  -  ( 1st `  p
) ) ) `  x )  =  ( ( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) `  x
) )
317313, 316oveq12d 6321 . . . . . 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 6321 . . . . 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 12187 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  (
0 ... J )  e. 
Fin )
320294adantrr 722 . . . . . 6  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  ( 0 ... J )  /\  c  e.  ( ( C `  R ) `  k ) ) )  ->  ( J  _C  k )  e.  CC )
321296anasss 652 . . . . . 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 9665 . . . . 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 13825 . . . 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 6331 . . . . . . . . 9  |-  ( J  -  ( c `  Z ) )  e. 
_V
325301resex 5165 . . . . . . . . 9  |-  ( c  |`  R