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

Theorem dvnprodlem3 37391
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 13941 . . . . . . . . 9  |-  ( s  =  (/)  ->  prod_ t  e.  s  ( ( H `  t ) `  x )  =  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) )
21mpteq2dv 4513 . . . . . . . 8  |-  ( s  =  (/)  ->  ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) )  =  ( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) )
32oveq2d 6321 . . . . . . 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 5883 . . . . . 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 5881 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( D `
 s )  =  ( D `  (/) ) )
65fveq1d 5883 . . . . . . . . 9  |-  ( s  =  (/)  ->  ( ( D `  s ) `
 k )  =  ( ( D `  (/) ) `  k ) )
76sumeq1d 13745 . . . . . . . 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 13941 . . . . . . . . . . 11  |-  ( s  =  (/)  ->  prod_ t  e.  s  ( ! `  ( c `  t
) )  =  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )
98oveq2d 6321 . . . . . . . . . 10  |-  ( s  =  (/)  ->  ( ( ! `  k )  /  prod_ t  e.  s  ( ! `  (
c `  t )
) )  =  ( ( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) ) )
10 prodeq1 13941 . . . . . . . . . 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 6323 . . . . . . . . 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 37218 . . . . . . . 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 2470 . . . . . . 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 4513 . . . . . 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 2451 . . . . 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 2871 . . . 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 13941 . . . . . . . . 9  |-  ( s  =  r  ->  prod_ t  e.  s  ( ( H `  t ) `
 x )  = 
prod_ t  e.  r 
( ( H `  t ) `  x
) )
1817mpteq2dv 4513 . . . . . . . 8  |-  ( s  =  r  ->  (
x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
)  =  ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) ) )
1918oveq2d 6321 . . . . . . 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 5883 . . . . . 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 5881 . . . . . . . . . 10  |-  ( s  =  r  ->  ( D `  s )  =  ( D `  r ) )
2221fveq1d 5883 . . . . . . . . 9  |-  ( s  =  r  ->  (
( D `  s
) `  k )  =  ( ( D `
 r ) `  k ) )
2322sumeq1d 13745 . . . . . . . 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 13941 . . . . . . . . . . 11  |-  ( s  =  r  ->  prod_ t  e.  s  ( ! `
 ( c `  t ) )  = 
prod_ t  e.  r 
( ! `  (
c `  t )
) )
2524oveq2d 6321 . . . . . . . . . 10  |-  ( s  =  r  ->  (
( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  r  ( ! `
 ( c `  t ) ) ) )
26 prodeq1 13941 . . . . . . . . . 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 6323 . . . . . . . . 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 37218 . . . . . . . 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 2470 . . . . . . 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 4513 . . . . . 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 2451 . . . . 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 2871 . . . 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 13941 . . . . . . . . 9  |-  ( s  =  ( r  u. 
{ z } )  ->  prod_ t  e.  s  ( ( H `  t ) `  x
)  =  prod_ t  e.  ( r  u.  {
z } ) ( ( H `  t
) `  x )
)
3433mpteq2dv 4513 . . . . . . . 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 6321 . . . . . . 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 5883 . . . . . 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 5881 . . . . . . . . . 10  |-  ( s  =  ( r  u. 
{ z } )  ->  ( D `  s )  =  ( D `  ( r  u.  { z } ) ) )
3837fveq1d 5883 . . . . . . . . 9  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( D `
 s ) `  k )  =  ( ( D `  (
r  u.  { z } ) ) `  k ) )
3938sumeq1d 13745 . . . . . . . 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 13941 . . . . . . . . . . 11  |-  ( s  =  ( r  u. 
{ z } )  ->  prod_ t  e.  s  ( ! `  (
c `  t )
)  =  prod_ t  e.  ( r  u.  {
z } ) ( ! `  ( c `
 t ) ) )
4140oveq2d 6321 . . . . . . . . . 10  |-  ( s  =  ( r  u. 
{ z } )  ->  ( ( ! `
 k )  /  prod_ t  e.  s  ( ! `  ( c `
 t ) ) )  =  ( ( ! `  k )  /  prod_ t  e.  ( r  u.  { z } ) ( ! `
 ( c `  t ) ) ) )
42 prodeq1 13941 . . . . . . . . . 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 6323 . . . . . . . . 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 37218 . . . . . . . 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 2470 . . . . . . 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 4513 . . . . . 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 2451 . . . . 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 2871 . . . 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 13941 . . . . . . . . . 10  |-  ( s  =  T  ->  prod_ t  e.  s  ( ( H `  t ) `
 x )  = 
prod_ t  e.  T  ( ( H `  t ) `  x
) )
5049mpteq2dv 4513 . . . . . . . . 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 2437 . . . . . . . . 9  |-  ( s  =  T  ->  (
x  e.  X  |->  prod_
t  e.  T  ( ( H `  t
) `  x )
)  =  F )
5450, 53eqtrd 2470 . . . . . . . 8  |-  ( s  =  T  ->  (
x  e.  X  |->  prod_
t  e.  s  ( ( H `  t
) `  x )
)  =  F )
5554oveq2d 6321 . . . . . . 7  |-  ( s  =  T  ->  ( S  Dn ( x  e.  X  |->  prod_ t  e.  s  ( ( H `  t ) `  x ) ) )  =  ( S  Dn F ) )
5655fveq1d 5883 . . . . . 6  |-  ( s  =  T  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  s 
( ( H `  t ) `  x
) ) ) `  k )  =  ( ( S  Dn
F ) `  k
) )
57 fveq2 5881 . . . . . . . . . 10  |-  ( s  =  T  ->  ( D `  s )  =  ( D `  T ) )
5857fveq1d 5883 . . . . . . . . 9  |-  ( s  =  T  ->  (
( D `  s
) `  k )  =  ( ( D `
 T ) `  k ) )
5958sumeq1d 13745 . . . . . . . 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 13941 . . . . . . . . . . 11  |-  ( s  =  T  ->  prod_ t  e.  s  ( ! `
 ( c `  t ) )  = 
prod_ t  e.  T  ( ! `  ( c `
 t ) ) )
6160oveq2d 6321 . . . . . . . . . 10  |-  ( s  =  T  ->  (
( ! `  k
)  /  prod_ t  e.  s  ( ! `  ( c `  t
) ) )  =  ( ( ! `  k )  /  prod_ t  e.  T  ( ! `
 ( c `  t ) ) ) )
62 prodeq1 13941 . . . . . . . . . 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 6323 . . . . . . . . 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 37218 . . . . . . . 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 2470 . . . . . . 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 4513 . . . . . 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 2451 . . . . 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 2871 . . . 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 13975 . . . . . . . . . . . . 13  |-  prod_ t  e.  (/)  ( ( H `
 t ) `  x )  =  1
7069mpteq2i 4509 . . . . . . . . . . . 12  |-  ( x  e.  X  |->  prod_ t  e.  (/)  ( ( H `
 t ) `  x ) )  =  ( x  e.  X  |->  1 )
7170oveq2i 6316 . . . . . . . . . . 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 23 . . . . . . . . . 10  |-  ( k  =  0  ->  k  =  0 )
7472, 73fveq12d 5887 . . . . . . . . 9  |-  ( k  =  0  ->  (
( S  Dn
( x  e.  X  |-> 
prod_ t  e.  (/)  ( ( H `  t ) `
 x ) ) ) `  k )  =  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  0 ) )
7574adantl 467 . . . . . . . 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 22736 . . . . . . . . . . 11  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
7876, 77syl 17 . . . . . . . . . 10  |-  ( ph  ->  S  C_  CC )
79 1cnd 9658 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  X )  ->  1  e.  CC )
80 eqid 2429 . . . . . . . . . . . . . 14  |-  ( x  e.  X  |->  1 )  =  ( x  e.  X  |->  1 )
8179, 80fmptd 6061 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  X  |->  1 ) : X --> CC )
82 1re 9641 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
8382rgenw 2793 . . . . . . . . . . . . . . . 16  |-  A. x  e.  X  1  e.  RR
84 dmmptg 5352 . . . . . . . . . . . . . . . 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 5733 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC  <->  ( x  e.  X  |->  1 ) : X --> CC ) )
8881, 87mpbird 235 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC )
89 restsspw 15289 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  S )  C_  ~P S
90 dvnprodlem3.x . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
9189, 90sseldi 3468 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  ~P S
)
92 elpwi 3994 . . . . . . . . . . . . . 14  |-  ( X  e.  ~P S  ->  X  C_  S )
9391, 92syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  X  C_  S )
9486, 93eqsstrd 3504 . . . . . . . . . . . 12  |-  ( ph  ->  dom  ( x  e.  X  |->  1 )  C_  S )
9588, 94jca 534 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  X  |->  1 ) : dom  ( x  e.  X  |->  1 ) --> CC 
/\  dom  ( x  e.  X  |->  1 ) 
C_  S ) )
96 cnex 9619 . . . . . . . . . . . . 13  |-  CC  e.  _V
9796a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
98 elpm2g 7496 . . . . . . . . . . . 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 665 . . . . . . . . . . 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 235 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  X  |->  1 )  e.  ( CC  ^pm  S )
)
101 dvn0 22755 . . . . . . . . . 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 665 . . . . . . . . 9  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  1 ) ) `
 0 )  =  ( x  e.  X  |->  1 ) )
103102adantr 466 . . . . . . . 8  |-  ( (
ph  /\  k  = 
0 )  ->  (
( S  Dn
( x  e.  X  |->  1 ) ) ` 
0 )  =  ( x  e.  X  |->  1 ) )
104 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( D `  (/) ) `  k )  =  ( ( D `  (/) ) ` 
0 ) )
105104adantl 467 . . . . . . . . . . . . . 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 6313 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  s )  =  ( ( 0 ... n )  ^m  (/) ) )
109 elmapfn 7502 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  Fn  (/) )
110 fn0 5713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  Fn  (/)  <->  x  =  (/) )
111109, 110sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  =  (/) )
112 elsn 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { (/) }  <->  x  =  (/) )
113111, 112sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  ->  x  e.  {
(/) } )
114112biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  { (/) }  ->  x  =  (/) )
115 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  (/)  ->  x  =  (/) )
116 f0 5781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/) : (/) --> ( 0 ... n )
117 ovex 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 0 ... n )  e. 
_V
118 0ex 4557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (/)  e.  _V
119117, 118elmap 7508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  ( ( 0 ... n )  ^m  (/) )  <->  (/) : (/) --> ( 0 ... n ) )
120116, 119mpbir 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  (/)  e.  ( ( 0 ... n
)  ^m  (/) )
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  (/)  ->  (/)  e.  ( ( 0 ... n
)  ^m  (/) ) )
122115, 121eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  (/)  ->  x  e.  ( ( 0 ... n )  ^m  (/) ) )
123114, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  { (/) }  ->  x  e.  ( ( 0 ... n )  ^m  (/) ) )
124113, 123impbii 190 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( ( 0 ... n )  ^m  (/) )  <->  x  e.  { (/) } )
125124ax-gen 1665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. x
( x  e.  ( ( 0 ... n
)  ^m  (/) )  <->  x  e.  {
(/) } )
126 dfcleq 2422 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 0 ... n
)  ^m  (/) )  =  { (/) }  <->  A. x
( x  e.  ( ( 0 ... n
)  ^m  (/) )  <->  x  e.  {
(/) } ) )
127125, 126mpbir 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0 ... n )  ^m  (/) )  =  { (/)
}
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  (/) )  =  { (/)
} )
129108, 128eqtrd 2470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  (/)  ->  ( ( 0 ... n )  ^m  s )  =  { (/) } )
130 rabeq 3081 . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . 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 13733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  (/)  ->  sum_ t  e.  s  ( c `  t )  =  sum_ t  e.  (/)  ( c `
 t ) )
133132eqeq1d 2431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  (/)  ->  ( sum_ t  e.  s  (
c `  t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  n ) )
134133rabbidv 3079 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  (/)  ->  { c  e.  { (/) }  |  sum_ t  e.  s  ( c `  t )  =  n }  =  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } )
135131, 134eqtrd 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  (/)  ->  { c  e.  ( ( 0 ... n )  ^m  s )  |  sum_ t  e.  s  (
c `  t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  n }
)
136135mpteq2dv 4513 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 4594 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  ~P T
139138a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
(/)  e.  ~P T
)
140 nn0ex 10875 . . . . . . . . . . . . . . . . . . 19  |-  NN0  e.  _V
141140mptex 6151 . . . . . . . . . . . . . . . . . 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 5970 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  (/) )  =  ( n  e.  NN0  |->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n } ) )
144 eqeq2 2444 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  0  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  0 ) )
145144rabbidv 3079 . . . . . . . . . . . . . . . . 17  |-  ( n  =  0  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
146145adantl 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  = 
0 )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
147 0nn0 10884 . . . . . . . . . . . . . . . . 17  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  NN0 )
149 p0ex 4612 . . . . . . . . . . . . . . . . . 18  |-  { (/) }  e.  _V
150149rabex 4576 . . . . . . . . . . . . . . . . 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 5970 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D `  (/) ) `  0 )  =  { c  e. 
{ (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 } )
153152adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) ` 
0 )  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 } )
154 snidg 4028 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  e.  _V  ->  (/)  e.  { (/)
} )
155118, 154ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  (/)  e.  { (/)
}
156 eqid 2429 . . . . . . . . . . . . . . . . . . . . 21  |-  0  =  0
157155, 156pm3.2i 456 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/)  e.  { (/) }  /\  0  =  0 )
158 sum0 13765 . . . . . . . . . . . . . . . . . . . . . . 23  |-  sum_ t  e.  (/)  ( c `  t )  =  0
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  =  (/)  ->  sum_ t  e.  (/)  ( c `  t )  =  0 )
160159eqeq1d 2431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  (/)  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  0  <->  0  =  0 ) )
161160elrab 3235 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/)  e.  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  0 }  <->  ( (/)  e.  { (/)
}  /\  0  = 
0 ) )
162157, 161mpbir 212 . . . . . . . . . . . . . . . . . . 19  |-  (/)  e.  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }
163162ne0ii 3774 . . . . . . . . . . . . . . . . . 18  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =/=  (/)
164163neii 2629 . . . . . . . . . . . . . . . . 17  |-  -.  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }  =  (/)
165 eqid 2429 . . . . . . . . . . . . . . . . . 18  |-  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  0 }
166 rabrsn 4073 . . . . . . . . . . . . . . . . . 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 1649 . . . . . . . . . . . . . . . 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 3921 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  if ( k  =  0 ,  { (/) } ,  (/) )  =  { (/) } )
171170adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  = 
0 )  ->  if ( k  =  0 ,  { (/) } ,  (/) )  =  { (/) } )
172169, 171eqtr4d 2473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  = 
0 )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  0 }  =  if ( k  =  0 ,  { (/) } ,  (/) ) )
173105, 153, 1723eqtrd 2474 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) `  k )  =  if ( k  =  0 ,  { (/) } ,  (/) ) )
174173, 171eqtrd 2470 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (/) ) `  k )  =  { (/)
} )
175174sumeq1d 13745 . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  ( ! `  k )  =  ( ! ` 
0 ) )
177 fac0 12459 . . . . . . . . . . . . . . . . . . 19  |-  ( ! `
 0 )  =  1
178177a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  ( ! `  0 )  =  1 )
179176, 178eqtrd 2470 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  ( ! `  k )  =  1 )
180179oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  =  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) ) )
181 prod0 13975 . . . . . . . . . . . . . . . . . 18  |-  prod_ t  e.  (/)  ( ! `  ( c `  t
) )  =  1
182181oveq2i 6316 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  =  ( 1  /  1 )
183 1div1e1 10299 . . . . . . . . . . . . . . . . 17  |-  ( 1  /  1 )  =  1
184182, 183eqtri 2458 . . . . . . . . . . . . . . . 16  |-  ( 1  /  prod_ t  e.  (/)  ( ! `  ( c `
 t ) ) )  =  1
185180, 184syl6eq 2486 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( ! `  k
)  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  =  1 )
186 prod0 13975 . . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( ( ! `  k )  /  prod_ t  e.  (/)  ( ! `  ( c `  t
) ) )  x. 
prod_ t  e.  (/)  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  x )
)  =  ( 1  x.  1 ) )
189188ad2antlr 731 . . . . . . . . . . . . 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 10757 . . . . . . . . . . . . . 14  |-  ( 1  x.  1 )  =  1
191190a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  =  0 )  /\  c  e.  { (/) } )  ->  ( 1  x.  1 )  =  1 )
192189, 191eqtrd 2470 . . . . . . . . . . . 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 13747 . . . . . . . . . . 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 9596 . . . . . . . . . . . . 13  |-  1  e.  CC
195 eqidd 2430 . . . . . . . . . . . . . 14  |-  ( c  =  (/)  ->  1  =  1 )
196195sumsn 13785 . . . . . . . . . . . . 13  |-  ( (
(/)  e.  _V  /\  1  e.  CC )  ->  sum_ c  e.  { (/) } 1  =  1 )
197118, 194, 196mp2an 676 . . . . . . . . . . . 12  |-  sum_ c  e.  { (/) } 1  =  1
198197a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
0 )  ->  sum_ c  e.  { (/) } 1  =  1 )
199175, 193, 1983eqtrd 2474 . . . . . . . . . 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 4513 . . . . . . . . 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 2437 . . . . . . . 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 2474 . . . . . . 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 26 . . . . . 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 5882 . . . . . . . . 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 466 . . . . . . . . . 10  |-  ( (
ph  /\  -.  k  =  0 )  ->  S  e.  { RR ,  CC } )
207206adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  S  e.  { RR ,  CC }
)
20890adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  -.  k  =  0 )  ->  X  e.  ( ( TopOpen
` fld
)t 
S ) )
209208adantr 466 . . . . . . . . 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 11885 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
212211adantl 467 . . . . . . . . . . . 12  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN0 )
213 neqne 37013 . . . . . . . . . . . . 13  |-  ( -.  k  =  0  -> 
k  =/=  0 )
214213adantr 466 . . . . . . . . . . . 12  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  =/=  0 )
215212, 214jca 534 . . . . . . . . . . 11  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  ( k  e.  NN0  /\  k  =/=  0 ) )
216 elnnne0 10883 . . . . . . . . . . 11  |-  ( k  e.  NN  <->  ( k  e.  NN0  /\  k  =/=  0 ) )
217215, 216sylibr 215 . . . . . . . . . 10  |-  ( ( -.  k  =  0  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN )
218217adantll 718 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  k  e.  NN )
219207, 209, 210, 218dvnmptconst 37384 . . . . . . . 8  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( x  e.  X  |->  1 ) ) `  k )  =  ( x  e.  X  |->  0 ) )
220143ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( D `  (/) )  =  ( n  e.  NN0  |->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n } ) )
221 eqeq2 2444 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  ( sum_ t  e.  (/)  ( c `
 t )  =  n  <->  sum_ t  e.  (/)  ( c `  t
)  =  k ) )
222221rabbidv 3079 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k } )
223222adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  {
c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k } )
224 eqidd 2430 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  k  =  k )
225 id 23 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  sum_ t  e.  (/)  ( c `  t
)  =  k )
226225eqcomd 2437 . . . . . . . . . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( sum_ t  e.  (/)  ( c `
 t )  =  k  ->  k  = 
0 )
229228adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( c  e.  { (/) }  /\  sum_ t  e.  (/)  ( c `  t
)  =  k )  ->  k  =  0 )
230229adantll 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -.  k  =  0  /\  c  e. 
{ (/) } )  /\  sum_ t  e.  (/)  ( c `
 t )  =  k )  ->  k  =  0 )
231 simpll 758 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -.  k  =  0  /\  c  e. 
{ (/) } )  /\  sum_ t  e.  (/)  ( c `
 t )  =  k )  ->  -.  k  =  0 )
232230, 231pm2.65da 578 . . . . . . . . . . . . . . . . . 18  |-  ( ( -.  k  =  0  /\  c  e.  { (/)
} )  ->  -.  sum_ t  e.  (/)  ( c `
 t )  =  k )
233232ralrimiva 2846 . . . . . . . . . . . . . . . . 17  |-  ( -.  k  =  0  ->  A. c  e.  { (/) }  -.  sum_ t  e.  (/)  ( c `  t
)  =  k )
234 rabeq0 3790 . . . . . . . . . . . . . . . . 17  |-  ( { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `  t
)  =  k }  =  (/)  <->  A. c  e.  { (/)
}  -.  sum_ t  e.  (/)  ( c `  t )  =  k )
235233, 234sylibr 215 . . . . . . . . . . . . . . . 16  |-  ( -.  k  =  0  ->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  k }  =  (/) )
236235adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  k }  =  (/) )
237223, 236eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( ( -.  k  =  0  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  (/) )
238237adantll 718 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  n  =  k )  ->  { c  e.  { (/) }  |  sum_ t  e.  (/)  ( c `
 t )  =  n }  =  (/) )
239238adantlr 719 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  -.  k  =  0
)  /\  k  e.  ( 0 ... N
) )  /\  n  =  k )  ->  { c  e.  { (/)
}  |  sum_ t  e.  (/)  ( c `  t )  =  n }  =  (/) )
240211adantl 467 . . . . . . . . . . . 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 5970 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  k  =  0 )  /\  k  e.  ( 0 ... N ) )  ->  ( ( D `  (/) ) `  k )  =  (/) )
243242sumeq1d 13745 . . . . . . . . . 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 13765 . . . . . . . . . . 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 2471 . . . . . . . . 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 4513 . . . . . . . 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 2474 . . . . . . 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 435 . . . . . 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 798 . . . . 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 2844 . . . 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 758 . . . . . . . 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 5881 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( H `  t
) `  x )  =  ( ( H `
 t ) `  y ) )
254253prodeq2ad 37243 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( H `  t ) `
 x )  = 
prod_ t  e.  r 
( ( H `  t ) `  y
) )
255 fveq2 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  ( H `  t )  =  ( H `  u ) )
256255fveq1d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  u  ->  (
( H `  t
) `  y )  =  ( ( H `
 u ) `  y ) )
257256cbvprodv 13948 . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  prod_ t  e.  r  ( ( H `  t ) `
 x )  = 
prod_ u  e.  r 
( ( H `  u ) `  y
) )
260259cbvmptv 4518 . . . . . . . . . . . . . 14  |-  ( x  e.  X  |->  prod_ t  e.  r  ( ( H `  t ) `  x ) )  =  ( y  e.  X  |-> 
prod_ u  e.  r 
( ( H `  u ) `  y
) )
261260oveq2i 6316 . . . . . . . . . . . . 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 5882 . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  u  ->  (
c `  t )  =  ( c `  u ) )
264263fveq2d 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  ( ! `  ( c `  t ) )  =  ( ! `  (
c `  u )
) )
265264cbvprodv 13948 . . . . . . . . . . . . . . . . . 18  |-  prod_ t  e.  r  ( ! `  ( c `  t
) )  =  prod_ u  e.  r  ( ! `
 ( c `  u ) )
266265oveq2i 6316 . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  x
)  =  ( ( ( S  Dn
( H `  t
) ) `  (
c `  t )
) `  y )
)
269268prodeq2ad 37243 . . . . . . . . . . . . . . . . 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 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  u  ->  ( S  Dn ( H `
 t ) )  =  ( S  Dn ( H `  u ) ) )
271270, 263fveq12d 5887 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  u  ->  (
( S  Dn
( H `  t
) ) `  (
c `  t )
)  =  ( ( S  Dn ( H `  u ) ) `  ( c `
 u ) ) )
272271fveq1d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  u  ->  (
( ( S  Dn ( H `  t ) ) `  ( c `  t
) ) `  y
)  =  ( ( ( S  Dn
( H `  u
) ) `  (
c `  u )
) `  y )
)
273272cbvprodv 13948 . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . 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 37218 . . . . . . . . . . . . . 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 5880 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  d  ->  (
c `  u )  =  ( d `  u ) )
279278fveq2d 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  d  ->  ( ! `  ( c `  u ) )  =  ( ! `  (
d `  u )
) )
280279prodeq2ad 37243 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  d  ->  prod_ u  e.  r  ( ! `
 ( c `  u ) )  = 
prod_ u  e.  r 
( ! `  (
d `  u )
) )
281280oveq2d 6321 . . . . . . . . . . . . . . . . 17  |-  ( c  =  d  ->  (
( ! `  k
)  /  prod_ u  e.  r  ( ! `  ( c `  u
) ) )  =  ( ( ! `  k )  /  prod_ u  e.  r  ( ! `
 ( d `  u ) ) ) )
282278fveq2d 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  d  ->  (
( S  Dn
( H `  u
) ) `  (
c `  u )
)  =  ( ( S  Dn ( H `  u ) ) `  ( d `
 u ) ) )
283282fveq1d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  d  ->  (
( ( S  Dn ( H `  u ) ) `  ( c `  u
) ) `  y
)  =  ( ( ( S  Dn
( H `  u
) ) `  (
d `  u )
) `  y )
)
284283prodeq2ad 37243 . . . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . . 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 13740 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . 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 4518 . . . . . . . . . . . 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 2449 . . . . . . . . . . 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 2863 . . . . . . . . . 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 197 . . . . . . . . 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 731 . . . . . . . 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 462 . . . . . . . 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 734 . . . . . . . . 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 734 . . . . . . . . 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 734 . . . . . . . . 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 774 . . . . . . . . . 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 )
( ( ( ! `