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

Theorem dvnprodlem3 31987
Description: The multinomial formula for the  k-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem3.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
dvnprodlem3.x  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
dvnprodlem3.t  |-  ( ph  ->  T  e.  Fin )
dvnprodlem3.h  |-  ( (
ph  /\  t  e.  T )  ->  ( H `  t ) : X --> CC )
dvnprodlem3.n  |-  ( ph  ->  N  e.  NN0 )
dvnprodlem3.dvnh  |-  ( (
ph  /\  t  e.  T  /\  j  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `
 t ) ) `
 j ) : X --> CC )
dvnprodlem3.f  |-  F  =  ( x  e.  X  |-> 
prod_ t  e.  T  ( ( H `  t ) `  x
) )
dvnprodlem3.d  |-  D  =  ( s  e.  ~P T  |->  ( n  e. 
NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s
)  |  sum_ t  e.  s  ( c `  t )  =  n } ) )
dvnprodlem3.c  |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  T )  |  sum_ t  e.  T  ( c `  t
)  =  n }
)
Assertion
Ref Expression
dvnprodlem3  |-  ( ph  ->  ( ( S  Dn F ) `  N )  =  ( x  e.  X  |->  sum_ c  e.  ( C `
 N ) ( ( ( ! `  N )  /  prod_ t  e.  T  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  T  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) )
Distinct variable groups:    C, c    D, c, j, t, n, s, x    F, s    H, c, j, t, n, s, x    N, c, j, t, n, s, x    S, c, j, t, n, s, x    T, c, j, t, n, s, x    X, c, j, t, n, s, x    ph, c,
j, t, n, s, x
Allowed substitution hints:    C( x, t, j, n, s)    F( x, t, j, n, c)

Proof of Theorem dvnprodlem3
Dummy variables  d  h  k  l  r 
z  y  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodeq1 13801 . . . . . . . . 9  |-  ( s  =  (/)  ->  prod_ t  e.  s  ( ( H `  t ) `  x )  =  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) )
21mpteq2dv 4526 . . . . . . . 8  |-  ( s  =  (/)  ->  ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) )  =  ( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) )
32oveq2d 6286 . . . . . . 7  |-  ( s  =  (/)  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) )  =  ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `  t ) `  x
) ) ) )
43fveq1d 5850 . . . . . 6  |-  ( s  =  (/)  ->  ( ( S  Dn ( x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
) ) `  k
)  =  ( ( S  Dn ( x  e.  X  |->  prod_
t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k ) )
5 fveq2 5848 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( D `
 s )  =  ( D `  (/) ) )
65fveq1d 5850 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( ( D `  s ) `
 k )  =  ( ( D `  (/) ) `  k ) )
76sumeq1d 13608 . . . . . . . 8  |-  ( s  =  (/)  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
8 prodeq1 13801 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  prod_ t  e.  s  ( ! `  ( c `  t
) )  =  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )
98oveq2d 6286 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  =  ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) ) )
10 prodeq1 13801 . . . . . . . . . 10  |-  ( s  =  (/)  ->  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )  =  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
119, 10oveq12d 6288 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( ( ( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  s 
( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
1211sumeq2ad 31808 . . . . . . . 8  |-  ( s  =  (/)  ->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
137, 12eqtrd 2495 . . . . . . 7  |-  ( s  =  (/)  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
1413mpteq2dv 4526 . . . . . 6  |-  ( s  =  (/)  ->  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
154, 14eqeq12d 2476 . . . . 5  |-  ( s  =  (/)  ->  ( ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <-> 
( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
1615ralbidv 2893 . . . 4  |-  ( s  =  (/)  ->  ( A. k  e.  ( 0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <->  A. k  e.  (
0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
17 prodeq1 13801 . . . . . . . . 9  |-  ( s  =  r  ->  prod_ t  e.  s  ( ( H `  t ) `
 x )  = 
prod_ t  e.  r 
( ( H `  t ) `  x
) )
1817mpteq2dv 4526 . . . . . . . 8  |-  ( s  =  r  ->  (
x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
)  =  ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) )
1918oveq2d 6286 . . . . . . 7  |-  ( s  =  r  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) )  =  ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x
) ) ) )
2019fveq1d 5850 . . . . . 6  |-  ( s  =  r  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  r 
( ( H `  t ) `  x
) ) ) `  k ) )
21 fveq2 5848 . . . . . . . . . 10  |-  ( s  =  r  ->  ( D `  s )  =  ( D `  r ) )
2221fveq1d 5850 . . . . . . . . 9  |-  ( s  =  r  ->  (
( D `  s
) `  k )  =  ( ( D `
 r ) `  k ) )
2322sumeq1d 13608 . . . . . . . 8  |-  ( s  =  r  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
24 prodeq1 13801 . . . . . . . . . . 11  |-  ( s  =  r  ->  prod_ t  e.  s  ( ! `
 ( c `  t ) )  = 
prod_ t  e.  r 
( ! `  (
c `  t )
) )
2524oveq2d 6286 . . . . . . . . . 10  |-  ( s  =  r  ->  (
( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) ) )
26 prodeq1 13801 . . . . . . . . . 10  |-  ( s  =  r  ->  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )  =  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
2725, 26oveq12d 6288 . . . . . . . . 9  |-  ( s  =  r  ->  (
( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  ( ( ( ! `
 k )  /  prod_ t  e.  r  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
2827sumeq2ad 31808 . . . . . . . 8  |-  ( s  =  r  ->  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
2923, 28eqtrd 2495 . . . . . . 7  |-  ( s  =  r  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
3029mpteq2dv 4526 . . . . . 6  |-  ( s  =  r  ->  (
x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  r  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
3120, 30eqeq12d 2476 . . . . 5  |-  ( s  =  r  ->  (
( ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <-> 
( ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) ) )
3231ralbidv 2893 . . . 4  |-  ( s  =  r  ->  ( A. k  e.  (
0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <->  A. k  e.  (
0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  r 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) ) )
33 prodeq1 13801 . . . . . . . . 9  |-  ( s  =  ( r  u. 
{ z } )  ->  prod_ t  e.  s  ( ( H `  t ) `  x
)  =  prod_ t  e.  ( r  u.  {
z } ) ( ( H `  t
) `  x )
)
3433mpteq2dv 4526 . . . . . . . 8  |-  ( s  =  ( r  u. 
{ z } )  ->  ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x
) )  =  ( x  e.  X  |->  prod_
t  e.  ( r  u.  { z } ) ( ( H `
 t ) `  x ) ) )
3534oveq2d 6286 . . . . . . 7  |-  ( s  =  ( r  u. 
{ z } )  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x
) ) )  =  ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (
r  u.  { z } ) ( ( H `  t ) `
 x ) ) ) )
3635fveq1d 5850 . . . . . 6  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) ) `
 k )  =  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  ( r  u.  { z } ) ( ( H `  t ) `
 x ) ) ) `  k ) )
37 fveq2 5848 . . . . . . . . . 10  |-  ( s  =  ( r  u. 
{ z } )  ->  ( D `  s )  =  ( D `  ( r  u.  { z } ) ) )
3837fveq1d 5850 . . . . . . . . 9  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( D `
 s ) `  k )  =  ( ( D `  (
r  u.  { z } ) ) `  k ) )
3938sumeq1d 13608 . . . . . . . 8  |-  ( s  =  ( r  u. 
{ z } )  ->  sum_ c  e.  ( ( D `  s
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  ( r  u.  {
z } ) ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
40 prodeq1 13801 . . . . . . . . . . 11  |-  ( s  =  ( r  u. 
{ z } )  ->  prod_ t  e.  s  ( ! `  (
c `  t )
)  =  prod_ t  e.  ( r  u.  {
z } ) ( ! `  ( c `
 t ) ) )
4140oveq2d 6286 . . . . . . . . . 10  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  =  ( ( ! `  k )  /  prod_ t  e.  ( r  u.  { z } ) ( ! `
 ( c `  t ) ) ) )
42 prodeq1 13801 . . . . . . . . . 10  |-  ( s  =  ( r  u. 
{ z } )  ->  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x )  =  prod_ t  e.  ( r  u. 
{ z } ) ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
4341, 42oveq12d 6288 . . . . . . . . 9  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  ( ( ( ! `  k
)  /  prod_ t  e.  ( r  u.  {
z } ) ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  ( r  u.  {
z } ) ( ( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  x
) ) )
4443sumeq2ad 31808 . . . . . . . 8  |-  ( s  =  ( r  u. 
{ z } )  ->  sum_ c  e.  ( ( D `  (
r  u.  { z } ) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  s 
( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  = 
sum_ c  e.  ( ( D `  (
r  u.  { z } ) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  ( r  u.  {
z } ) ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  ( r  u.  {
z } ) ( ( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  x
) ) )
4539, 44eqtrd 2495 . . . . . . 7  |-  ( s  =  ( r  u. 
{ z } )  ->  sum_ c  e.  ( ( D `  s
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  ( r  u.  {
z } ) ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  ( r  u. 
{ z } ) ( ! `  (
c `  t )
) )  x.  prod_ t  e.  ( r  u. 
{ z } ) ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
4645mpteq2dv 4526 . . . . . 6  |-  ( s  =  ( r  u. 
{ z } )  ->  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  ( r  u.  { z } ) ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  ( r  u.  { z } ) ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  ( r  u.  { z } ) ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
4736, 46eqeq12d 2476 . . . . 5  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( ( S  Dn ( x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
) ) `  k
)  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  <->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  ( r  u.  {
z } ) ( ( H `  t
) `  x )
) ) `  k
)  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  ( r  u.  {
z } ) ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  ( r  u. 
{ z } ) ( ! `  (
c `  t )
) )  x.  prod_ t  e.  ( r  u. 
{ z } ) ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) ) )
4847ralbidv 2893 . . . 4  |-  ( s  =  ( r  u. 
{ z } )  ->  ( A. k  e.  ( 0 ... N
) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  s
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  s  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  <->  A. k  e.  ( 0 ... N
) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  ( r  u.  {
z } ) ( ( H `  t
) `  x )
) ) `  k
)  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  ( r  u.  {
z } ) ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  ( r  u. 
{ z } ) ( ! `  (
c `  t )
) )  x.  prod_ t  e.  ( r  u. 
{ z } ) ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) ) )
49 prodeq1 13801 . . . . . . . . . 10  |-  ( s  =  T  ->  prod_ t  e.  s  ( ( H `  t ) `
 x )  = 
prod_ t  e.  T  ( ( H `  t ) `  x
) )
5049mpteq2dv 4526 . . . . . . . . 9  |-  ( s  =  T  ->  (
x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
)  =  ( x  e.  X  |->  prod_ t  e.  T  ( ( H `  t ) `  x ) ) )
51 dvnprodlem3.f . . . . . . . . . . 11  |-  F  =  ( x  e.  X  |-> 
prod_ t  e.  T  ( ( H `  t ) `  x
) )
5251a1i 11 . . . . . . . . . 10  |-  ( s  =  T  ->  F  =  ( x  e.  X  |->  prod_ t  e.  T  ( ( H `  t ) `  x
) ) )
5352eqcomd 2462 . . . . . . . . 9  |-  ( s  =  T  ->  (
x  e.  X  |->  prod_
t  e.  T  ( ( H `  t
) `  x )
)  =  F )
5450, 53eqtrd 2495 . . . . . . . 8  |-  ( s  =  T  ->  (
x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
)  =  F )
5554oveq2d 6286 . . . . . . 7  |-  ( s  =  T  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) )  =  ( S  Dn F ) )
5655fveq1d 5850 . . . . . 6  |-  ( s  =  T  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( ( S  Dn
F ) `  k
) )
57 fveq2 5848 . . . . . . . . . 10  |-  ( s  =  T  ->  ( D `  s )  =  ( D `  T ) )
5857fveq1d 5850 . . . . . . . . 9  |-  ( s  =  T  ->  (
( D `  s
) `  k )  =  ( ( D `
 T ) `  k ) )
5958sumeq1d 13608 . . . . . . . 8  |-  ( s  =  T  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  T ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
60 prodeq1 13801 . . . . . . . . . . 11  |-  ( s  =  T  ->  prod_ t  e.  s  ( ! `
 ( c `  t ) )  = 
prod_ t  e.  T  ( ! `  ( c `
 t ) ) )
6160oveq2d 6286 . . . . . . . . . 10  |-  ( s  =  T  ->  (
( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  T  ( ! `
 ( c `  t ) ) ) )
62 prodeq1 13801 . . . . . . . . . 10  |-  ( s  =  T  ->  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )  =  prod_ t  e.  T  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )
6361, 62oveq12d 6288 . . . . . . . . 9  |-  ( s  =  T  ->  (
( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  ( ( ( ! `
 k )  /  prod_ t  e.  T  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  T  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
6463sumeq2ad 31808 . . . . . . . 8  |-  ( s  =  T  ->  sum_ c  e.  ( ( D `  T ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  T ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  T  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  T  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
6559, 64eqtrd 2495 . . . . . . 7  |-  ( s  =  T  ->  sum_ c  e.  ( ( D `  s ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  s  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  T ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  T  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  T  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
6665mpteq2dv 4526 . . . . . 6  |-  ( s  =  T  ->  (
x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  T
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  T  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  T  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
6756, 66eqeq12d 2476 . . . . 5  |-  ( s  =  T  ->  (
( ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <-> 
( ( S  Dn F ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  T ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  T  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  T  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) ) )
6867ralbidv 2893 . . . 4  |-  ( s  =  T  ->  ( A. k  e.  (
0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  s ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  s  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  s  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <->  A. k  e.  (
0 ... N ) ( ( S  Dn
F ) `  k
)  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  T ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  T  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  T  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
69 prod0 13835 . . . . . . . . . . . . 13  |-  prod_ t  e.  (/)  ( ( H `
 t ) `  x )  =  1
7069mpteq2i 4522 . . . . . . . . . . . 12  |-  ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) )  =  ( x  e.  X  |->  1 )
7170oveq2i 6281 . . . . . . . . . . 11  |-  ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) )  =  ( S  Dn ( x  e.  X  |->  1 ) )
7271a1i 11 . . . . . . . . . 10  |-  ( k  =  0  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) )  =  ( S  Dn ( x  e.  X  |->  1 ) ) )
73 id 22 . . . . . . . . . 10  |-  ( k  =  0  ->  k  =  0 )
7472, 73fveq12d 5854 . . . . . . . . 9  |-  ( k  =  0  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  0 ) )
7574adantl 464 . . . . . . . 8  |-  ( (
ph  /\  k  = 
0 )  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  0 ) )
76 dvnprodlem3.s . . . . . . . . . . 11  |-  ( ph  ->  S  e.  { RR ,  CC } )
77 recnprss 22477 . . . . . . . . . . 11  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
7876, 77syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  C_  CC )
79 1cnd 9601 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  X )  ->  1  e.  CC )
80 eqid 2454 . . . . . . . . . . . . . 14  |-  ( x  e.  X  |->  1 )  =  ( x  e.  X  |->  1 )
8179, 80fmptd 6031 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  X  |->  1 ) : X --> CC )
82 1re 9584 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
8382rgenw 2815 . . . . . . . . . . . . . . . 16  |-  A. x  e.  X  1  e.  RR
84 dmmptg 5487 . . . . . . . . . . . . . . . 16  |-  ( A. x  e.  X  1  e.  RR  ->  dom  ( x  e.  X  |->  1 )  =  X )
8583, 84ax-mp 5 . . . . . . . . . . . . . . 15  |-  dom  (
x  e.  X  |->  1 )  =  X
8685a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( x  e.  X  |->  1 )  =  X )
8786feq2d 5700 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC  <->  ( x  e.  X  |->  1 ) : X --> CC ) )
8881, 87mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC )
89 restsspw 14924 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  S )  C_  ~P S
90 dvnprodlem3.x . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
9189, 90sseldi 3487 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  ~P S
)
92 elpwi 4008 . . . . . . . . . . . . . 14  |-  ( X  e.  ~P S  ->  X  C_  S )
9391, 92syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  X  C_  S )
9486, 93eqsstrd 3523 . . . . . . . . . . . 12  |-  ( ph  ->  dom  ( x  e.  X  |->  1 )  C_  S )
9588, 94jca 530 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC 
/\  dom  ( x  e.  X  |->  1 ) 
C_  S ) )
96 cnex 9562 . . . . . . . . . . . . 13  |-  CC  e.  _V
9796a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
98 elpm2g 7428 . . . . . . . . . . . 12  |-  ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  -> 
( ( x  e.  X  |->  1 )  e.  ( CC  ^pm  S
)  <->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC  /\  dom  (
x  e.  X  |->  1 )  C_  S )
) )
9997, 76, 98syl2anc 659 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  X  |->  1 )  e.  ( CC  ^pm  S
)  <->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC  /\  dom  (
x  e.  X  |->  1 )  C_  S )
) )
10095, 99mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  X  |->  1 )  e.  ( CC  ^pm  S )
)
101 dvn0 22496 . . . . . . . . . 10  |-  ( ( S  C_  CC  /\  (
x  e.  X  |->  1 )  e.  ( CC 
^pm  S ) )  ->  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  0 )  =  ( x  e.  X  |->  1 ) )
10278, 100, 101syl2anc 659 . . . . . . . . 9  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  1 ) ) `
 0 )  =  ( x  e.  X  |->  1 ) )
103102adantr 463 . . . . . . . 8  |-  ( (
ph  /\  k  = 
0 )  ->  (
( S  Dn
( x  e.  X  |->  1 ) ) ` 
0 )  =  ( x  e.  X  |->  1 ) )
104 fveq2 5848 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( D `  (/) ) `  k )  =  ( ( D `  (/) ) ` 
0 ) )
105104adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) `  k )  =  ( ( D `  (/) ) ` 
0 ) )
106 dvnprodlem3.d . . . . . . . . . . . . . . . . . 18  |-  D  =  ( s  e.  ~P T  |->  ( n  e. 
NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s
)  |  sum_ t  e.  s  ( c `  t )  =  n } ) )
107106a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  D  =  ( s  e.  ~P T  |->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n } ) ) )
108 oveq2 6278 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  s )  =  ( ( 0 ... n )  ^m  (/) ) )
109 elmapfn 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  Fn  (/) )
110 fn0 5682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  Fn  (/)  <->  x  =  (/) )
111109, 110sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  =  (/) )
112 elsn 4030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { (/) }  <->  x  =  (/) )
113111, 112sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  e.  {
(/) } )
114112biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { (/) }  ->  x  =  (/) )
115 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  (/)  ->  x  =  (/) )
116 f0 5748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/) : (/) --> ( 0 ... n )
117 ovex 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0 ... n )  e. 
_V
118 0ex 4569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (/)  e.  _V
119117, 118elmap 7440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  ( ( 0 ... n )  ^m  (/) )  <->  (/) : (/) --> ( 0 ... n ) )
120116, 119mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  (/)  e.  ( ( 0 ... n
)  ^m  (/) )
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  (/)  ->  (/)  e.  ( ( 0 ... n
)  ^m  (/) ) )
122115, 121eqeltrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  (/)  ->  x  e.  ( ( 0 ... n )  ^m  (/) ) )
123114, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  { (/) }  ->  x  e.  ( ( 0 ... n )  ^m  (/) ) )
124113, 123impbii 188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  <->  x  e.  { (/) } )
125124ax-gen 1623 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. x
( x  e.  ( ( 0 ... n
)  ^m  (/) )  <->  x  e.  {
(/) } )
126 dfcleq 2447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 0 ... n
)  ^m  (/) )  =  { (/) }  <->  A. x
( x  e.  ( ( 0 ... n
)  ^m  (/) )  <->  x  e.  {
(/) } ) )
127125, 126mpbir 209 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0 ... n )  ^m  (/) )  =  { (/)
}
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  (/) )  =  { (/)
} )
129108, 128eqtrd 2495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  s )  =  { (/) } )
130 rabeq 3100 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 0 ... n
)  ^m  s )  =  { (/) }  ->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  s  ( c `  t
)  =  n }
)
131129, 130syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  (/)  ->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  s  ( c `  t
)  =  n }
)
132 sumeq1 13596 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  (/)  ( c `
 t ) )
133132eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  (/)  ->  ( sum_ t  e.  s  (
c `  t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  n ) )
134133rabbidv 3098 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  (/)  ->  { c  e.  { (/) }  |  sum_ t  e.  s  ( c `  t )  =  n }  =  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } )
135131, 134eqtrd 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  (/)  ->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  n }
)
136135mpteq2dv 4526 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  (/)  ->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n } )  =  ( n  e.  NN0  |->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } ) )
137136adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  =  (/) )  ->  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  s
)  |  sum_ t  e.  s  ( c `  t )  =  n } )  =  ( n  e.  NN0  |->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n } ) )
138 0elpw 4606 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  ~P T
139138a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
(/)  e.  ~P T
)
140 nn0ex 10797 . . . . . . . . . . . . . . . . . . 19  |-  NN0  e.  _V
141140mptex 6118 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN0  |->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n } )  e. 
_V
142141a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( n  e.  NN0  |->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } )  e.  _V )
143107, 137, 139, 142fvmptd 5936 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  (/) )  =  ( n  e.  NN0  |->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } ) )
144 eqeq2 2469 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  0  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  0 ) )
145144rabbidv 3098 . . . . . . . . . . . . . . . . 17  |-  ( n  =  0  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
146145adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  = 
0 )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
147 0nn0 10806 . . . . . . . . . . . . . . . . 17  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  NN0 )
149 p0ex 4624 . . . . . . . . . . . . . . . . . 18  |-  { (/) }  e.  _V
150149rabex 4588 . . . . . . . . . . . . . . . . 17  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  e.  _V
151150a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  0 }  e.  _V )
152143, 146, 148, 151fvmptd 5936 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D `  (/) ) `  0 )  =  { c  e. 
{ (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 } )
153152adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) ` 
0 )  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
154 snidg 4042 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  e.  _V  ->  (/)  e.  { (/)
} )
155118, 154ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  (/)  e.  { (/)
}
156 eqid 2454 . . . . . . . . . . . . . . . . . . . . 21  |-  0  =  0
157155, 156pm3.2i 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/)  e.  { (/) }  /\  0  =  0 )
158 sum0 13628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  sum_ t  e.  (/)  ( c `  t )  =  0
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  =  (/)  ->  sum_ t  e.  (/)  ( c `  t )  =  0 )
160159eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  (/)  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  0  <->  0  =  0 ) )
161160elrab 3254 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/)  e.  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  0 }  <->  ( (/)  e.  { (/)
}  /\  0  = 
0 ) )
162157, 161mpbir 209 . . . . . . . . . . . . . . . . . . 19  |-  (/)  e.  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }
163162ne0ii 3790 . . . . . . . . . . . . . . . . . 18  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =/=  (/)
164163neii 2653 . . . . . . . . . . . . . . . . 17  |-  -.  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }  =  (/)
165 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }
166 rabrsn 4086 . . . . . . . . . . . . . . . . . 18  |-  ( { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }  =  { c  e. 
{ (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  ->  ( { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  0 }  =  (/)  \/  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }  =  { (/) } ) )
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }  =  (/)  \/  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  { (/)
} )
168164, 167mtpor 1607 . . . . . . . . . . . . . . . 16  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  { (/)
}
169168a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  = 
0 )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  { (/)
} )
170 iftrue 3935 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  if ( k  =  0 ,  { (/) } ,  (/) )  =  { (/) } )
171170adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  = 
0 )  ->  if ( k  =  0 ,  { (/) } ,  (/) )  =  { (/) } )
172169, 171eqtr4d 2498 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  = 
0 )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  if ( k  =  0 ,  { (/) } ,  (/) ) )
173105, 153, 1723eqtrd 2499 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) `  k )  =  if ( k  =  0 ,  { (/) } ,  (/) ) )
174173, 171eqtrd 2495 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) `  k )  =  { (/)
} )
175174sumeq1d 13608 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
0 )  ->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  = 
sum_ c  e.  { (/)
}  ( ( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x ) ) )
176 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  ( ! `  k )  =  ( ! ` 
0 ) )
177 fac0 12341 . . . . . . . . . . . . . . . . . . 19  |-  ( ! `
 0 )  =  1
178177a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  ( ! `  0 )  =  1 )
179176, 178eqtrd 2495 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  ( ! `  k )  =  1 )
180179oveq1d 6285 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  =  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) ) )
181 prod0 13835 . . . . . . . . . . . . . . . . . 18  |-  prod_ t  e.  (/)  ( ! `  ( c `  t
) )  =  1
182181oveq2i 6281 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  =  ( 1  /  1 )
183 1div1e1 10233 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  1 )  =  1
184182, 183eqtri 2483 . . . . . . . . . . . . . . . 16  |-  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  =  1
185180, 184syl6eq 2511 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  =  1 )
186 prod0 13835 . . . . . . . . . . . . . . . 16  |-  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x )  =  1
187186a1i 11 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x )  =  1 )
188185, 187oveq12d 6288 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  ( 1  x.  1 ) )
189188ad2antlr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  =  0 )  /\  c  e.  { (/) } )  ->  ( ( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x ) )  =  ( 1  x.  1 ) )
190 1t1e1 10679 . . . . . . . . . . . . . 14  |-  ( 1  x.  1 )  =  1
191190a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  =  0 )  /\  c  e.  { (/) } )  ->  ( 1  x.  1 )  =  1 )
192189, 191eqtrd 2495 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  =  0 )  /\  c  e.  { (/) } )  ->  ( ( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x ) )  =  1 )
193192sumeq2dv 13610 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
0 )  ->  sum_ c  e.  { (/) }  ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  { (/) } 1 )
194 ax-1cn 9539 . . . . . . . . . . . . 13  |-  1  e.  CC
195 eqidd 2455 . . . . . . . . . . . . . 14  |-  ( c  =  (/)  ->  1  =  1 )
196195sumsn 13648 . . . . . . . . . . . . 13  |-  ( (
(/)  e.  _V  /\  1  e.  CC )  ->  sum_ c  e.  { (/) } 1  =  1 )
197118, 194, 196mp2an 670 . . . . . . . . . . . 12  |-  sum_ c  e.  { (/) } 1  =  1
198197a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
0 )  ->  sum_ c  e.  { (/) } 1  =  1 )
199175, 193, 1983eqtrd 2499 . . . . . . . . . 10  |-  ( (
ph  /\  k  = 
0 )  ->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  1 )
200199mpteq2dv 4526 . . . . . . . . 9  |-  ( (
ph  /\  k  = 
0 )  ->  (
x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  =  ( x  e.  X  |->  1 ) )
201200eqcomd 2462 . . . . . . . 8  |-  ( (
ph  /\  k  = 
0 )  ->  (
x  e.  X  |->  1 )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) ) )
20275, 103, 2013eqtrd 2499 . . . . . . 7  |-  ( (
ph  /\  k  = 
0 )  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
203202a1d 25 . . . . . 6  |-  ( (
ph  /\  k  = 
0 )  ->  (
k  e.  ( 0 ... N )  -> 
( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
20471fveq1i 5849 . . . . . . . . 9  |-  ( ( S  Dn ( x  e.  X  |->  prod_
t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  k )
205204a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) ) `
 k )  =  ( ( S  Dn ( x  e.  X  |->  1 ) ) `
 k ) )
20676adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  -.  k  =  0 )  ->  S  e.  { RR ,  CC } )
207206adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  S  e.  { RR ,  CC }
)
20890adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  -.  k  =  0 )  ->  X  e.  ( ( TopOpen
` fld
)t 
S ) )
209208adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  X  e.  ( ( TopOpen ` fld )t  S ) )
210194a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  1  e.  CC )
211 elfznn0 11775 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
212211adantl 464 . . . . . . . . . . . 12  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN0 )
213 neqne 31677 . . . . . . . . . . . . 13  |-  ( -.  k  =  0  -> 
k  =/=  0 )
214213adantr 463 . . . . . . . . . . . 12  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  =/=  0 )
215212, 214jca 530 . . . . . . . . . . 11  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  ( k  e.  NN0  /\  k  =/=  0 ) )
216 elnnne0 10805 . . . . . . . . . . 11  |-  ( k  e.  NN  <->  ( k  e.  NN0  /\  k  =/=  0 ) )
217215, 216sylibr 212 . . . . . . . . . 10  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN )
218217adantll 711 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN )
219207, 209, 210, 218dvnmptconst 31980 . . . . . . . 8  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  k )  =  ( x  e.  X  |->  0 ) )
220143ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( D `  (/) )  =  ( n  e.  NN0  |->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n } ) )
221 eqeq2 2469 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  k ) )
222221rabbidv 3098 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k } )
223222adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k } )
224 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  k  =  k )
225 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  sum_ t  e.  (/)  ( c `  t
)  =  k )
226225eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  k  =  sum_ t  e.  (/)  ( c `
 t ) )
227158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  sum_ t  e.  (/)  ( c `  t
)  =  0 )
228224, 226, 2273eqtrd 2499 . . . . . . . . . . . . . . . . . . . . 21  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  k  = 
0 )
229228adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  { (/) }  /\  sum_ t  e.  (/)  ( c `  t
)  =  k )  ->  k  =  0 )
230229adantll 711 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -.  k  =  0  /\  c  e. 
{ (/) } )  /\  sum_ t  e.  (/)  ( c `
 t )  =  k )  ->  k  =  0 )
231 simpll 751 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -.  k  =  0  /\  c  e. 
{ (/) } )  /\  sum_ t  e.  (/)  ( c `
 t )  =  k )  ->  -.  k  =  0 )
232230, 231pm2.65da 574 . . . . . . . . . . . . . . . . . 18  |-  ( ( -.  k  =  0  /\  c  e.  { (/)
} )  ->  -.  sum_ t  e.  (/)  ( c `
 t )  =  k )
233232ralrimiva 2868 . . . . . . . . . . . . . . . . 17  |-  ( -.  k  =  0  ->  A. c  e.  { (/) }  -.  sum_ t  e.  (/)  ( c `  t
)  =  k )
234 rabeq0 3806 . . . . . . . . . . . . . . . . 17  |-  ( { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k }  =  (/)  <->  A. c  e.  { (/)
}  -.  sum_ t  e.  (/)  ( c `  t )  =  k )
235233, 234sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( -.  k  =  0  ->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  k }  =  (/) )
236235adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  k }  =  (/) )
237223, 236eqtrd 2495 . . . . . . . . . . . . . 14  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  (/) )
238237adantll 711 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  (/) )
239238adantlr 712 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  -.  k  =  0
)  /\  k  e.  ( 0 ... N
) )  /\  n  =  k )  ->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n }  =  (/) )
240211adantl 464 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN0 )
241118a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  (/)  e.  _V )
242220, 239, 240, 241fvmptd 5936 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( D `  (/) ) `  k )  =  (/) )
243242sumeq1d 13608 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  = 
sum_ c  e.  (/)  ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )
244 sum0 13628 . . . . . . . . . . 11  |-  sum_ c  e.  (/)  ( ( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `  t ) ) `  ( c `
 t ) ) `
 x ) )  =  0
245244a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  sum_ c  e.  (/)  ( ( ( ! `
 k )  /  prod_ t  e.  (/)  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  (/)  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  0 )
246243, 245eqtr2d 2496 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  0  =  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )
247246mpteq2dv 4526 . . . . . . . 8  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( x  e.  X  |->  0 )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
248205, 219, 2473eqtrd 2499 . . . . . . 7  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
249248ex 432 . . . . . 6  |-  ( (
ph  /\  -.  k  =  0 )  -> 
( k  e.  ( 0 ... N )  ->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
250203, 249pm2.61dan 789 . . . . 5  |-  ( ph  ->  ( k  e.  ( 0 ... N )  ->  ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) ) )
251250ralrimiv 2866 . . . 4  |-  ( ph  ->  A. k  e.  ( 0 ... N ) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  (/) ) `  k ) ( ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )
252 simpll 751 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  r  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) ) )
253 fveq2 5848 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( H `  t
) `  x )  =  ( ( H `
 t ) `  y ) )
254253prodeq2ad 31832 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( H `  t ) `
 x )  = 
prod_ t  e.  r 
( ( H `  t ) `  y
) )
255 fveq2 5848 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  ( H `  t )  =  ( H `  u ) )
256255fveq1d 5850 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  u  ->  (
( H `  t
) `  y )  =  ( ( H `
 u ) `  y ) )
257256cbvprodv 13808 . . . . . . . . . . . . . . . . 17  |-  prod_ t  e.  r  ( ( H `  t ) `  y )  =  prod_ u  e.  r  ( ( H `  u ) `
 y )
258257a1i 11 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( H `  t ) `
 y )  = 
prod_ u  e.  r 
( ( H `  u ) `  y
) )
259254, 258eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( H `  t ) `
 x )  = 
prod_ u  e.  r 
( ( H `  u ) `  y
) )
260259cbvmptv 4530 . . . . . . . . . . . . . 14  |-  ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) )  =  ( y  e.  X  |-> 
prod_ u  e.  r 
( ( H `  u ) `  y
) )
261260oveq2i 6281 . . . . . . . . . . . . 13  |-  ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) )  =  ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y
) ) )
262261fveq1i 5849 . . . . . . . . . . . 12  |-  ( ( S  Dn ( x  e.  X  |->  prod_
t  e.  r  ( ( H `  t
) `  x )
) ) `  k
)  =  ( ( S  Dn ( y  e.  X  |->  prod_
u  e.  r  ( ( H `  u
) `  y )
) ) `  k
)
263 fveq2 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  u  ->  (
c `  t )  =  ( c `  u ) )
264263fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  ( ! `  ( c `  t ) )  =  ( ! `  (
c `  u )
) )
265264cbvprodv 13808 . . . . . . . . . . . . . . . . . 18  |-  prod_ t  e.  r  ( ! `  ( c `  t
) )  =  prod_ u  e.  r  ( ! `
 ( c `  u ) )
266265oveq2i 6281 . . . . . . . . . . . . . . . . 17  |-  ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  =  ( ( ! `  k
)  /  prod_ u  e.  r  ( ! `  ( c `  u
) ) )
267266a1i 11 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( ! `  k
)  /  prod_ t  e.  r  ( ! `  ( c `  t
) ) )  =  ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( c `  u ) ) ) )
268 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  x
)  =  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  y )
)
269268prodeq2ad 31832 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )  =  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  y ) )
270255oveq2d 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  u  ->  ( S  Dn ( H `
 t ) )  =  ( S  Dn ( H `  u ) ) )
271270, 263fveq12d 5854 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  u  ->  (
( S  Dn
( H `  t
) ) `  (
c `  t )
)  =  ( ( S  Dn ( H `  u ) ) `  ( c `
 u ) ) )
272271fveq1d 5850 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  (
( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  y
)  =  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
)
273272cbvprodv 13808 . . . . . . . . . . . . . . . . . 18  |-  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  y )  =  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( c `  u ) ) `  y )
274273a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  y )  =  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( c `  u ) ) `  y ) )
275269, 274eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )  =  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( c `  u ) ) `  y ) )
276267, 275oveq12d 6288 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) )  =  ( ( ( ! `
 k )  /  prod_ u  e.  r  ( ! `  ( c `
 u ) ) )  x.  prod_ u  e.  r  ( (
( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
) )
277276sumeq2ad 31808 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
c `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
) )
278 fveq1 5847 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  d  ->  (
c `  u )  =  ( d `  u ) )
279278fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  d  ->  ( ! `  ( c `  u ) )  =  ( ! `  (
d `  u )
) )
280279prodeq2ad 31832 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  d  ->  prod_ u  e.  r  ( ! `
 ( c `  u ) )  = 
prod_ u  e.  r 
( ! `  (
d `  u )
) )
281280oveq2d 6286 . . . . . . . . . . . . . . . . 17  |-  ( c  =  d  ->  (
( ! `  k
)  /  prod_ u  e.  r  ( ! `  ( c `  u
) ) )  =  ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) ) )
282278fveq2d 5852 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  d  ->  (
( S  Dn
( H `  u
) ) `  (
c `  u )
)  =  ( ( S  Dn ( H `  u ) ) `  ( d `
 u ) ) )
283282fveq1d 5850 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  d  ->  (
( ( S  Dn ( H `  u ) ) `  ( c `  u
) ) `  y
)  =  ( ( ( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
)
284283prodeq2ad 31832 . . . . . . . . . . . . . . . . 17  |-  ( c  =  d  ->  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )  =  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) )
285281, 284oveq12d 6288 . . . . . . . . . . . . . . . 16  |-  ( c  =  d  ->  (
( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( c `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( c `  u ) ) `  y ) )  =  ( ( ( ! `
 k )  /  prod_ u  e.  r  ( ! `  ( d `
 u ) ) )  x.  prod_ u  e.  r  ( (
( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) )
286285cbvsumv 13603 . . . . . . . . . . . . . . 15  |-  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
c `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
)  =  sum_ d  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
d `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
)
287286a1i 11 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
c `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
)  =  sum_ d  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
d `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) )
288277, 287eqtrd 2495 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  sum_ d  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `  (
d `  u )
) )  x.  prod_ u  e.  r  ( ( ( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) )
289288cbvmptv 4530 . . . . . . . . . . . 12  |-  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `  k
) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `  (
c `  t )
) )  x.  prod_ t  e.  r  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) )  =  ( y  e.  X  |->  sum_ d  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) ) )
290262, 289eqeq12i 2474 . . . . . . . . . . 11  |-  ( ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  r 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <-> 
( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y
) ) ) `  k )  =  ( y  e.  X  |->  sum_ d  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) ) ) )
291290ralbii 2885 . . . . . . . . . 10  |-  ( A. k  e.  ( 0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  r 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  <->  A. k  e.  (
0 ... N ) ( ( S  Dn
( y  e.  X  |-> 
prod_ u  e.  r 
( ( H `  u ) `  y
) ) ) `  k )  =  ( y  e.  X  |->  sum_ d  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) ) ) )
292291biimpi 194 . . . . . . . . 9  |-  ( A. k  e.  ( 0 ... N ) ( ( S  Dn
( x  e.  X  |-> 
prod_ t  e.  r 
( ( H `  t ) `  x
) ) ) `  k )  =  ( x  e.  X  |->  sum_ c  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) )  x.  prod_ t  e.  r  ( ( ( S  Dn ( H `
 t ) ) `
 ( c `  t ) ) `  x ) ) )  ->  A. k  e.  ( 0 ... N ) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y
) ) ) `  k )  =  ( y  e.  X  |->  sum_ d  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) ) ) )
293292ad2antlr 724 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  r  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  A. k  e.  ( 0 ... N ) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y
) ) ) `  k )  =  ( y  e.  X  |->  sum_ d  e.  ( ( D `  r ) `
 k ) ( ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) )  x.  prod_ u  e.  r  ( ( ( S  Dn ( H `
 u ) ) `
 ( d `  u ) ) `  y ) ) ) )
294 simpr 459 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) ) `
 k )  =  ( x  e.  X  |-> 
sum_ c  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ t  e.  r  ( ! `  ( c `
 t ) ) )  x.  prod_ t  e.  r  ( (
( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  j  e.  ( 0 ... N ) )
29576ad3antrrr 727 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y ) ) ) `
 k )  =  ( y  e.  X  |-> 
sum_ d  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ u  e.  r  ( ! `  ( d `
 u ) ) )  x.  prod_ u  e.  r  ( (
( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  S  e.  { RR ,  CC } )
29690ad3antrrr 727 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y ) ) ) `
 k )  =  ( y  e.  X  |-> 
sum_ d  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ u  e.  r  ( ! `  ( d `
 u ) ) )  x.  prod_ u  e.  r  ( (
( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  X  e.  ( ( TopOpen ` fld )t  S ) )
297 dvnprodlem3.t . . . . . . . . . 10  |-  ( ph  ->  T  e.  Fin )
298297ad3antrrr 727 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y ) ) ) `
 k )  =  ( y  e.  X  |-> 
sum_ d  e.  ( ( D `  r
) `  k )
( ( ( ! `
 k )  /  prod_ u  e.  r  ( ! `  ( d `
 u ) ) )  x.  prod_ u  e.  r  ( (
( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
) ) )  /\  j  e.  ( 0 ... N ) )  ->  T  e.  Fin )
299 simp-4l 765 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( r  C_  T  /\  z  e.  ( T  \  r ) ) )  /\  A. k  e.  ( 0 ... N
) ( ( S  Dn ( y  e.  X  |->  prod_ u  e.  r  ( ( H `  u ) `  y ) ) ) `
 k )  =  ( y  e.  X  |-> 
sum_ d  e.  ( ( D `  r
) `  k )
( ( (