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

Theorem dvnprodlem2 31983
Description: Induction step for dvnprodlem2 31983. (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 1712 . . . . . 6  |-  F/ t ( ph  /\  x  e.  X )
2 nfcv 2616 . . . . . 6  |-  F/_ t
( ( H `  Z ) `  x
)
3 dvnprodlem2.t . . . . . . . 8  |-  ( ph  ->  T  e.  Fin )
4 dvnprodlem2.r . . . . . . . 8  |-  ( ph  ->  R  C_  T )
5 ssfi 7733 . . . . . . . 8  |-  ( ( T  e.  Fin  /\  R  C_  T )  ->  R  e.  Fin )
63, 4, 5syl2anc 659 . . . . . . 7  |-  ( ph  ->  R  e.  Fin )
76adantr 463 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  R  e.  Fin )
8 dvnprodlem2.z . . . . . . 7  |-  ( ph  ->  Z  e.  ( T 
\  R ) )
98adantr 463 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  Z  e.  ( T  \  R
) )
108eldifbd 3474 . . . . . . 7  |-  ( ph  ->  -.  Z  e.  R
)
1110adantr 463 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  -.  Z  e.  R )
12 simpl 455 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  R )  ->  ph )
134sselda 3489 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  R )  ->  t  e.  T )
14 dvnprodlem2.h . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  ( H `  t ) : X --> CC )
1512, 13, 14syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  t  e.  R )  ->  ( H `  t ) : X --> CC )
1615adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  ( H `  t ) : X --> CC )
17 simplr 753 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  x  e.  X )
1816, 17ffvelrnd 6008 . . . . . 6  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  R )  ->  (
( H `  t
) `  x )  e.  CC )
19 fveq2 5848 . . . . . . 7  |-  ( t  =  Z  ->  ( H `  t )  =  ( H `  Z ) )
2019fveq1d 5850 . . . . . 6  |-  ( t  =  Z  ->  (
( H `  t
) `  x )  =  ( ( H `
 Z ) `  x ) )
21 id 22 . . . . . . . . 9  |-  ( ph  ->  ph )
22 eldifi 3612 . . . . . . . . . 10  |-  ( Z  e.  ( T  \  R )  ->  Z  e.  T )
238, 22syl 16 . . . . . . . . 9  |-  ( ph  ->  Z  e.  T )
24 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  Z  e.  T )  ->  Z  e.  T )
25 id 22 . . . . . . . . . 10  |-  ( (
ph  /\  Z  e.  T )  ->  ( ph  /\  Z  e.  T
) )
26 eleq1 2526 . . . . . . . . . . . . 13  |-  ( t  =  Z  ->  (
t  e.  T  <->  Z  e.  T ) )
2726anbi2d 701 . . . . . . . . . . . 12  |-  ( t  =  Z  ->  (
( ph  /\  t  e.  T )  <->  ( ph  /\  Z  e.  T ) ) )
2819feq1d 5699 . . . . . . . . . . . 12  |-  ( t  =  Z  ->  (
( H `  t
) : X --> CC  <->  ( H `  Z ) : X --> CC ) )
2927, 28imbi12d 318 . . . . . . . . . . 11  |-  ( t  =  Z  ->  (
( ( ph  /\  t  e.  T )  ->  ( H `  t
) : X --> CC )  <-> 
( ( ph  /\  Z  e.  T )  ->  ( H `  Z
) : X --> CC ) ) )
3029, 14vtoclg 3164 . . . . . . . . . 10  |-  ( Z  e.  T  ->  (
( ph  /\  Z  e.  T )  ->  ( H `  Z ) : X --> CC ) )
3124, 25, 30sylc 60 . . . . . . . . 9  |-  ( (
ph  /\  Z  e.  T )  ->  ( H `  Z ) : X --> CC )
3221, 23, 31syl2anc 659 . . . . . . . 8  |-  ( ph  ->  ( H `  Z
) : X --> CC )
3332adantr 463 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  ( H `  Z ) : X --> CC )
34 simpr 459 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  X )
3533, 34ffvelrnd 6008 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  (
( H `  Z
) `  x )  e.  CC )
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 31831 . . . . 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 4525 . . . 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 6286 . . 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 5850 . 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 31834 . . 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 11775 . . . 4  |-  ( J  e.  ( 0 ... N )  ->  J  e.  NN0 )
4543, 44syl 16 . . 3  |-  ( ph  ->  J  e.  NN0 )
46 eqid 2454 . . 3  |-  ( x  e.  X  |->  prod_ t  e.  R  ( ( H `  t ) `  x ) )  =  ( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
47 eqid 2454 . . 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 6278 . . . . . . . . . . . . . 14  |-  ( s  =  R  ->  (
( 0 ... n
)  ^m  s )  =  ( ( 0 ... n )  ^m  R ) )
51 rabeq 3100 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 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 13593 . . . . . . . . . . . . . . 15  |-  ( s  =  R  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  R  (
c `  t )
)
5453eqeq1d 2456 . . . . . . . . . . . . . 14  |-  ( s  =  R  ->  ( sum_ t  e.  s  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  n ) )
5554rabbidv 3098 . . . . . . . . . . . . 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 2495 . . . . . . . . . . . 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 4526 . . . . . . . . . . 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 464 . . . . . . . . . 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 4583 . . . . . . . . . . . . . 14  |-  ( ( R  C_  T  /\  T  e.  Fin )  ->  R  e.  _V )
604, 3, 59syl2anc 659 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  _V )
61 elpwg 4007 . . . . . . . . . . . . 13  |-  ( R  e.  _V  ->  ( R  e.  ~P T  <->  R 
C_  T ) )
6260, 61syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( R  e.  ~P T 
<->  R  C_  T )
)
634, 62mpbird 232 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  ~P T
)
6463adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  R  e.  ~P T )
65 nn0ex 10797 . . . . . . . . . . . 12  |-  NN0  e.  _V
6665mptex 6118 . . . . . . . . . . 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 5936 . . . . . . . . 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 6278 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
0 ... n )  =  ( 0 ... k
) )
7069oveq1d 6285 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( 0 ... n
)  ^m  R )  =  ( ( 0 ... k )  ^m  R ) )
71 rabeq 3100 . . . . . . . . . . . 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 16 . . . . . . . . . . 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 2469 . . . . . . . . . . . 12  |-  ( n  =  k  ->  ( sum_ t  e.  R  ( c `  t )  =  n  <->  sum_ t  e.  R  ( c `  t )  =  k ) )
7473rabbidv 3098 . . . . . . . . . . 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 2495 . . . . . . . . . 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 464 . . . . . . . . 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 11775 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  e.  NN0 )
7877adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  NN0 )
79 fzfid 12065 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... k
)  e.  Fin )
80 mapfi 7808 . . . . . . . . . . . 12  |-  ( ( ( 0 ... k
)  e.  Fin  /\  R  e.  Fin )  ->  ( ( 0 ... k )  ^m  R
)  e.  Fin )
8179, 6, 80syl2anc 659 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 0 ... k )  ^m  R
)  e.  Fin )
8281adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0 ... k
)  ^m  R )  e.  Fin )
83 ssrab2 3571 . . . . . . . . . . 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 4584 . . . . . . . . 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 5936 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  =  { c  e.  ( ( 0 ... k
)  ^m  R )  |  sum_ t  e.  R  ( c `  t
)  =  k } )
87 ssfi 7733 . . . . . . . . . 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 660 . . . . . . . . 9  |-  ( ph  ->  { c  e.  ( ( 0 ... k
)  ^m  R )  |  sum_ t  e.  R  ( c `  t
)  =  k }  e.  Fin )
8988adantr 463 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  { c  e.  ( ( 0 ... k )  ^m  R )  |  sum_ t  e.  R  (
c `  t )  =  k }  e.  Fin )
9086, 89eqeltrd 2542 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  e.  Fin )
9190adantr 463 . . . . . 6  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  ->  (
( C `  R
) `  k )  e.  Fin )
9277faccld 31755 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... J )  ->  ( ! `  k )  e.  NN )
9392nncnd 10547 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  ( ! `  k )  e.  CC )
9493ad2antlr 724 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  ( ! `  k )  e.  CC )
956adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
9695adantlr 712 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
97 elfznn0 11775 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( 0 ... k )  ->  z  e.  NN0 )
9897ssriv 3493 . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  c  e.  ( ( C `  R ) `  k
) )
10186eleq2d 2524 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . 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 3485 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  { c  e.  ( ( 0 ... k )  ^m  R
)  |  sum_ t  e.  R  ( c `  t )  =  k }  ->  c  e.  ( ( 0 ... k )  ^m  R
) )
105103, 104syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  c  e.  ( ( 0 ... k )  ^m  R
) )
106 elmapi 7433 . . . . . . . . . . . . . . . 16  |-  ( c  e.  ( ( 0 ... k )  ^m  R )  ->  c : R --> ( 0 ... k ) )
107105, 106syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  c : R --> ( 0 ... k ) )
108107adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  c : R --> ( 0 ... k ) )
109 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  t  e.  R )
110108, 109ffvelrnd 6008 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... k
) )
11199, 110sseldd 3490 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  NN0 )
112111faccld 31755 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  e.  NN )
113112nncnd 10547 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  e.  CC )
11496, 113fprodcl 13841 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  prod_ t  e.  R  ( ! `
 ( c `  t ) )  e.  CC )
115112nnne0d 10576 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  ( ! `  ( c `  t ) )  =/=  0 )
11696, 113, 115fprodn0 13865 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  prod_ t  e.  R  ( ! `
 ( c `  t ) )  =/=  0 )
11794, 114, 116divcld 10316 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  c  e.  ( ( C `  R ) `  k
) )  ->  (
( ! `  k
)  /  prod_ t  e.  R  ( ! `  ( c `  t
) ) )  e.  CC )
118117adantlr 712 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  ->  (
( ! `  k
)  /  prod_ t  e.  R  ( ! `  ( c `  t
) ) )  e.  CC )
11996adantlr 712 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  ->  R  e.  Fin )
12021ad4antr 729 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  ph )
121120, 13sylancom 665 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  t  e.  T )
122 elfzuz3 11688 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  J  e.  ( ZZ>= `  k )
)
123 fzss2 11727 . . . . . . . . . . . . . . . 16  |-  ( J  e.  ( ZZ>= `  k
)  ->  ( 0 ... k )  C_  ( 0 ... J
) )
124122, 123syl 16 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0 ... k )  C_  ( 0 ... J
) )
125124adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... k )  C_  ( 0 ... J
) )
12645nn0zd 10963 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  ZZ )
127 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  NN0 )
128127nn0zd 10963 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ZZ )
129 elfzle2 11693 . . . . . . . . . . . . . . . . . . 19  |-  ( J  e.  ( 0 ... N )  ->  J  <_  N )
13043, 129syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  <_  N )
131126, 128, 1303jca 1174 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( J  e.  ZZ  /\  N  e.  ZZ  /\  J  <_  N ) )
132 eluz2 11088 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  J
)  <->  ( J  e.  ZZ  /\  N  e.  ZZ  /\  J  <_  N ) )
133131, 132sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ( ZZ>= `  J ) )
134 fzss2 11727 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  J
)  ->  ( 0 ... J )  C_  ( 0 ... N
) )
135133, 134syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0 ... J
)  C_  ( 0 ... N ) )
136135adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... J )  C_  ( 0 ... N
) )
137125, 136sstrd 3499 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0 ... k )  C_  ( 0 ... N
) )
138137ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
0 ... k )  C_  ( 0 ... N
) )
139138, 110sseldd 3490 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  c  e.  ( ( C `  R
) `  k )
)  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... N
) )
140139adantllr 716 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  (
c `  t )  e.  ( 0 ... N
) )
141 fvex 5858 . . . . . . . . . . 11  |-  ( c `
 t )  e. 
_V
142 eleq1 2526 . . . . . . . . . . . . 13  |-  ( j  =  ( c `  t )  ->  (
j  e.  ( 0 ... N )  <->  ( c `  t )  e.  ( 0 ... N ) ) )
1431423anbi3d 1303 . . . . . . . . . . . 12  |-  ( j  =  ( c `  t )  ->  (
( ph  /\  t  e.  T  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  T  /\  ( c `  t
)  e.  ( 0 ... N ) ) ) )
144 fveq2 5848 . . . . . . . . . . . . 13  |-  ( j  =  ( c `  t )  ->  (
( S  Dn
( H `  t
) ) `  j
)  =  ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) )
145144feq1d 5699 . . . . . . . . . . . 12  |-  ( j  =  ( c `  t )  ->  (
( ( S  Dn ( H `  t ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) : X --> CC ) )
146143, 145imbi12d 318 . . . . . . . . . . 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 3158 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T  /\  ( c `  t )  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) : X --> CC )
149120, 121, 140, 148syl3anc 1226 . . . . . . . . 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 758 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  k  e.  ( 0 ... J ) )  /\  x  e.  X
)  /\  c  e.  ( ( C `  R ) `  k
) )  /\  t  e.  R )  ->  x  e.  X )
151149, 150ffvelrnd 6008 . . . . . . . 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 13841 . . . . . . 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 9605 . . . . . 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 13637 . . . . 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 2454 . . . . 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 6031 . . . 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 463 . . . . . 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 10872 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  0  e.  ZZ )
160128adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  N  e.  ZZ )
161 elfzelz 11691 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  e.  ZZ )
162161adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  ZZ )
163159, 160, 1623jca 1174 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ ) )
164 elfzle1 11692 . . . . . . . . 9  |-  ( k  e.  ( 0 ... J )  ->  0  <_  k )
165164adantl 464 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  0  <_  k )
166162zred 10965 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  RR )
16745nn0red 10849 . . . . . . . . . 10  |-  ( ph  ->  J  e.  RR )
168167adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  J  e.  RR )
169160zred 10965 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  N  e.  RR )
170 elfzle2 11693 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... J )  ->  k  <_  J )
171170adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  <_  J )
172130adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  J  <_  N )
173166, 168, 169, 171, 172letrd 9728 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  <_  N )
174163, 165, 173jca32 533 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  ( 0  <_  k  /\  k  <_  N ) ) )
175 elfz2 11682 . . . . . . 7  |-  ( k  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  (
0  <_  k  /\  k  <_  N ) ) )
176174, 175sylibr 212 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  k  e.  ( 0 ... N
) )
177 rspa 2821 . . . . . 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 659 . . . . 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 5699 . . . 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 232 . . 3  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) ) ) `  k ) : X --> CC )
18123adantr 463 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  Z  e.  T )
182 simpl 455 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ph )
183182, 181, 1763jca 1174 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( ph  /\  Z  e.  T  /\  k  e.  (
0 ... N ) ) )
184263anbi2d 1302 . . . . . . 7  |-  ( t  =  Z  ->  (
( ph  /\  t  e.  T  /\  k  e.  ( 0 ... N
) )  <->  ( ph  /\  Z  e.  T  /\  k  e.  ( 0 ... N ) ) ) )
18519oveq2d 6286 . . . . . . . . 9  |-  ( t  =  Z  ->  ( S  Dn ( H `
 t ) )  =  ( S  Dn ( H `  Z ) ) )
186185fveq1d 5850 . . . . . . . 8  |-  ( t  =  Z  ->  (
( S  Dn
( H `  t
) ) `  k
)  =  ( ( S  Dn ( H `  Z ) ) `  k ) )
187186feq1d 5699 . . . . . . 7  |-  ( t  =  Z  ->  (
( ( S  Dn ( H `  t ) ) `  k ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  k ) : X --> CC ) )
188184, 187imbi12d 318 . . . . . 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 2526 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  e.  ( 0 ... N )  <->  k  e.  ( 0 ... N
) ) )
1901893anbi3d 1303 . . . . . . . 8  |-  ( j  =  k  ->  (
( ph  /\  t  e.  T  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  T  /\  k  e.  ( 0 ... N ) ) ) )
191 fveq2 5848 . . . . . . . . 9  |-  ( j  =  k  ->  (
( S  Dn
( H `  t
) ) `  j
)  =  ( ( S  Dn ( H `  t ) ) `  k ) )
192191feq1d 5699 . . . . . . . 8  |-  ( j  =  k  ->  (
( ( S  Dn ( H `  t ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  t ) ) `  k ) : X --> CC ) )
193190, 192imbi12d 318 . . . . . . 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 2019 . . . . . 6  |-  ( (
ph  /\  t  e.  T  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `
 t ) ) `
 k ) : X --> CC )
195188, 194vtoclg 3164 . . . . 5  |-  ( Z  e.  T  ->  (
( ph  /\  Z  e.  T  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
( H `  Z
) ) `  k
) : X --> CC ) )
196181, 183, 195sylc 60 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  k
) : X --> CC )
19732feqmptd 5901 . . . . . . . . 9  |-  ( ph  ->  ( H `  Z
)  =  ( x  e.  X  |->  ( ( H `  Z ) `
 x ) ) )
198197eqcomd 2462 . . . . . . . 8  |-  ( ph  ->  ( x  e.  X  |->  ( ( H `  Z ) `  x
) )  =  ( H `  Z ) )
199198oveq2d 6286 . . . . . . 7  |-  ( ph  ->  ( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) )  =  ( S  Dn
( H `  Z
) ) )
200199fveq1d 5850 . . . . . 6  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( ( H `
 Z ) `  x ) ) ) `
 k )  =  ( ( S  Dn ( H `  Z ) ) `  k ) )
201200adantr 463 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) ) `  k )  =  ( ( S  Dn
( H `  Z
) ) `  k
) )
202201feq1d 5699 . . . 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 232 . . 3  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( x  e.  X  |->  ( ( H `  Z ) `  x
) ) ) `  k ) : X --> CC )
204 fveq2 5848 . . . . . . . 8  |-  ( y  =  x  ->  (
( H `  t
) `  y )  =  ( ( H `
 t ) `  x ) )
205204prodeq2ad 31829 . . . . . . 7  |-  ( y  =  x  ->  prod_ t  e.  R  ( ( H `  t ) `
 y )  = 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
206205cbvmptv 4530 . . . . . 6  |-  ( y  e.  X  |->  prod_ t  e.  R  ( ( H `  t ) `  y ) )  =  ( x  e.  X  |-> 
prod_ t  e.  R  ( ( H `  t ) `  x
) )
207206oveq2i 6281 . . . . 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 5849 . . . 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 4522 . . 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 5848 . . . . . . 7  |-  ( y  =  x  ->  (
( H `  Z
) `  y )  =  ( ( H `
 Z ) `  x ) )
211210cbvmptv 4530 . . . . . 6  |-  ( y  e.  X  |->  ( ( H `  Z ) `
 y ) )  =  ( x  e.  X  |->  ( ( H `
 Z ) `  x ) )
212211oveq2i 6281 . . . . 5  |-  ( S  Dn ( y  e.  X  |->  ( ( H `  Z ) `
 y ) ) )  =  ( S  Dn ( x  e.  X  |->  ( ( H `  Z ) `
 x ) ) )
213212fveq1i 5849 . . . 4  |-  ( ( S  Dn ( y  e.  X  |->  ( ( H `  Z
) `  y )
) ) `  k
)  =  ( ( S  Dn ( x  e.  X  |->  ( ( H `  Z
) `  x )
) ) `  k
)
214213mpteq2i 4522 . . 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 31979 . 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 2823 . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . 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 4525 . . . . . . . . . . . 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 6117 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 5941 . . . . . . . . . . 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 712 . . . . . . . . . 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 5850 . . . . . . . . 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 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  x  e.  X )
228154an32s 802 . . . . . . . . . 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 5939 . . . . . . . . . 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 659 . . . . . . . . 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 2495 . . . . . . . 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 5848 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) ) `  k )  =  ( ( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) ) `  j ) )
233232cbvmptv 4530 . . . . . . . . . . . . . 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 2507 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S  Dn
( y  e.  X  |->  ( ( H `  Z ) `  y
) ) )  =  ( S  Dn
( H `  Z
) ) )
236235fveq1d 5850 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( S  Dn ( y  e.  X  |->  ( ( H `
 Z ) `  y ) ) ) `
 j )  =  ( ( S  Dn ( H `  Z ) ) `  j ) )
237236mpteq2dv 4526 . . . . . . . . . . . . 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 2495 . . . . . . . . . . . 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 463 . . . . . . . . . . 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 5848 . . . . . . . . . . . 12  |-  ( j  =  ( J  -  k )  ->  (
( S  Dn
( H `  Z
) ) `  j
)  =  ( ( S  Dn ( H `  Z ) ) `  ( J  -  k ) ) )
241240adantl 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  j  =  ( J  -  k ) )  -> 
( ( S  Dn ( H `  Z ) ) `  j )  =  ( ( S  Dn
( H `  Z
) ) `  ( J  -  k )
) )
242 0zd 10872 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  0  e.  ZZ )
243 elfzel2 11689 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  J  e.  ZZ )
244243, 161zsubcld 10970 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  ( J  -  k )  e.  ZZ )
245242, 243, 2443jca 1174 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  (
0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k )  e.  ZZ ) )
246243zred 10965 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  J  e.  RR )
24777nn0red 10849 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... J )  ->  k  e.  RR )
248246, 247subge0d 10138 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0  <_  ( J  -  k )  <->  k  <_  J ) )
249170, 248mpbird 232 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  0  <_  ( J  -  k
) )
250246, 247subge02d 10140 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... J )  ->  (
0  <_  k  <->  ( J  -  k )  <_  J ) )
251164, 250mpbid 210 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... J )  ->  ( J  -  k )  <_  J )
252245, 249, 251jca32 533 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... J )  ->  (
( 0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( J  -  k
)  /\  ( J  -  k )  <_  J ) ) )
253252adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( 0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( J  -  k
)  /\  ( J  -  k )  <_  J ) ) )
254 elfz2 11682 . . . . . . . . . . . 12  |-  ( ( J  -  k )  e.  ( 0 ... J )  <->  ( (
0  e.  ZZ  /\  J  e.  ZZ  /\  ( J  -  k )  e.  ZZ )  /\  (
0  <_  ( J  -  k )  /\  ( J  -  k
)  <_  J )
) )
255253, 254sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  -  k )  e.  ( 0 ... J
) )
256 fvex 5858 . . . . . . . . . . . 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 5936 . . . . . . . . . 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 712 . . . . . . . . 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 5850 . . . . . . . 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 6288 . . . . . . 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 6286 . . . . . 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 712 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( C `  R
) `  k )  e.  Fin )
264 ovex 6298 . . . . . . . . . . . 12  |-  ( J  -  k )  e. 
_V
265 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( j  =  ( J  -  k )  ->  (
j  e.  ( 0 ... J )  <->  ( J  -  k )  e.  ( 0 ... J
) ) )
266265anbi2d 701 . . . . . . . . . . . . 13  |-  ( j  =  ( J  -  k )  ->  (
( ph  /\  j  e.  ( 0 ... J
) )  <->  ( ph  /\  ( J  -  k
)  e.  ( 0 ... J ) ) ) )
267240feq1d 5699 . . . . . . . . . . . . 13  |-  ( j  =  ( J  -  k )  ->  (
( ( S  Dn ( H `  Z ) ) `  j ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) : X --> CC ) )
268266, 267imbi12d 318 . . . . . . . . . . . 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 2526 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
k  e.  ( 0 ... J )  <->  j  e.  ( 0 ... J
) ) )
270269anbi2d 701 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ph  /\  k  e.  ( 0 ... J
) )  <->  ( ph  /\  j  e.  ( 0 ... J ) ) ) )
271 fveq2 5848 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( S  Dn
( H `  Z
) ) `  k
)  =  ( ( S  Dn ( H `  Z ) ) `  j ) )
272271feq1d 5699 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( S  Dn ( H `  Z ) ) `  k ) : X --> CC 
<->  ( ( S  Dn ( H `  Z ) ) `  j ) : X --> CC ) )
273270, 272imbi12d 318 . . . . . . . . . . . . 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 2019 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  j
) : X --> CC )
275264, 268, 274vtocl 3158 . . . . . . . . . . 11  |-  ( (
ph  /\  ( J  -  k )  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
276182, 255, 275syl2anc 659 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
277276adantlr 712 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( S  Dn
( H `  Z
) ) `  ( J  -  k )
) : X --> CC )
278277, 227ffvelrnd 6008 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  (
( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) `  x
)  e.  CC )
279 anass 647 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  <->  ( ph  /\  ( k  e.  ( 0 ... J )  /\  x  e.  X
) ) )
280 ancom 448 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( 0 ... J )  /\  x  e.  X )  <->  ( x  e.  X  /\  k  e.  ( 0 ... J ) ) )
281280anbi2i 692 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  ( 0 ... J
)  /\  x  e.  X ) )  <->  ( ph  /\  ( x  e.  X  /\  k  e.  (
0 ... J ) ) ) )
282 anass 647 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  <->  ( ph  /\  ( x  e.  X  /\  k  e.  (
0 ... J ) ) ) )
283282bicomi 202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  X  /\  k  e.  ( 0 ... J
) ) )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
284281, 283bitri 249 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  ( 0 ... J
)  /\  x  e.  X ) )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
285279, 284bitri 249 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 0 ... J
) )  /\  x  e.  X )  <->  ( ( ph  /\  x  e.  X
)  /\  k  e.  ( 0 ... J
) ) )
286285anbi1i 693 . . . . . . . . . 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 323 . . . . . . . . 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 208 . . . . . . . 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 13682 . . . . . . 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 6286 . . . . . 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 16 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  J  e.  NN0 )
292291, 162bccld 31759 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e. 
NN0 )
293292nn0cnd 10850 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e.  CC )
294293adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  ( 0 ... J
) )  ->  ( J  _C  k )  e.  CC )
295278adantr 463 . . . . . . . 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 9605 . . . . . . 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 13681 . . . . . 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 2499 . . . . 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 13607 . . . 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 3109 . . . . . . . 8  |-  k  e. 
_V
301 vex 3109 . . . . . . . 8  |-  c  e. 
_V
302300, 301op1std 6783 . . . . . . 7  |-  ( p  =  <. k ,  c
>.  ->  ( 1st `  p
)  =  k )
303302oveq2d 6286 . . . . . 6  |-  ( p  =  <. k ,  c
>.  ->  ( J  _C  ( 1st `  p ) )  =  ( J  _C  k ) )
304302fveq2d 5852 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( ! `  ( 1st `  p ) )  =  ( ! `
 k ) )
305300, 301op2ndd 6784 . . . . . . . . . . . 12  |-  ( p  =  <. k ,  c
>.  ->  ( 2nd `  p
)  =  c )
306305fveq1d 5850 . . . . . . . . . . 11  |-  ( p  =  <. k ,  c
>.  ->  ( ( 2nd `  p ) `  t
)  =  ( c `
 t ) )
307306fveq2d 5852 . . . . . . . . . 10  |-  ( p  =  <. k ,  c
>.  ->  ( ! `  ( ( 2nd `  p
) `  t )
)  =  ( ! `
 ( c `  t ) ) )
308307prodeq2ad 31829 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  prod_ t  e.  R  ( ! `  ( ( 2nd `  p ) `
 t ) )  =  prod_ t  e.  R  ( ! `  ( c `
 t ) ) )
309304, 308oveq12d 6288 . . . . . . . 8  |-  ( p  =  <. k ,  c
>.  ->  ( ( ! `
 ( 1st `  p
) )  /  prod_ t  e.  R  ( ! `
 ( ( 2nd `  p ) `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  R  ( ! `
 ( c `  t ) ) ) )
310306fveq2d 5852 . . . . . . . . . 10  |-  ( p  =  <. k ,  c
>.  ->  ( ( S  Dn ( H `
 t ) ) `
 ( ( 2nd `  p ) `  t
) )  =  ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) )
311310fveq1d 5850 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( ( ( S  Dn ( H `  t ) ) `  ( ( 2nd `  p ) `
 t ) ) `
 x )  =  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
312311prodeq2ad 31829 . . . . . . . 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 6288 . . . . . . 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 6286 . . . . . . . . 9  |-  ( p  =  <. k ,  c
>.  ->  ( J  -  ( 1st `  p ) )  =  ( J  -  k ) )
315314fveq2d 5852 . . . . . . . 8  |-  ( p  =  <. k ,  c
>.  ->  ( ( S  Dn ( H `
 Z ) ) `
 ( J  -  ( 1st `  p ) ) )  =  ( ( S  Dn
( H `  Z
) ) `  ( J  -  k )
) )
316315fveq1d 5850 . . . . . . 7  |-  ( p  =  <. k ,  c
>.  ->  ( ( ( S  Dn ( H `  Z ) ) `  ( J  -  ( 1st `  p
) ) ) `  x )  =  ( ( ( S  Dn ( H `  Z ) ) `  ( J  -  k
) ) `  x
) )
317313, 316oveq12d 6288 . . . . . 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 6288 . . . . 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 12065 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  (
0 ... J )  e. 
Fin )
320294adantrr 714 . . . . . 6  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  ( 0 ... J )  /\  c  e.  ( ( C `  R ) `  k ) ) )  ->  ( J  _C  k )  e.  CC )
321296anasss 645 . . . . . 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 9605 . . . . 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 13668 . . . 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 6298 . . . . . . . . 9  |-  ( J  -  ( c `  Z ) )  e. 
_V
325301resex 5305 . . . . . . . . 9  |-  ( c  |`