This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvnprodlem3

Description: The multinomial formula for the k -th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnprodlem3.s 
|- ( ph -> S e. { RR , CC } )
dvnprodlem3.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`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 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvnprodlem3.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnprodlem3.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvnprodlem3.t 
 |-  ( ph -> T e. Fin )
4 dvnprodlem3.h 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
5 dvnprodlem3.n 
 |-  ( ph -> N e. NN0 )
6 dvnprodlem3.dvnh 
 |-  ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )
7 dvnprodlem3.f 
 |-  F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) )
8 dvnprodlem3.d 
 |-  D = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )
9 dvnprodlem3.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )
10 prodeq1 
 |-  ( s = (/) -> prod_ t e. s ( ( H ` t ) ` x ) = prod_ t e. (/) ( ( H ` t ) ` x ) )
11 10 mpteq2dv 
 |-  ( s = (/) -> ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) )
12 11 oveq2d 
 |-  ( s = (/) -> ( S Dn ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) ) = ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) )
13 12 fveq1d 
 |-  ( 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 ) )
14 fveq2 
 |-  ( s = (/) -> ( D ` s ) = ( D ` (/) ) )
15 14 fveq1d 
 |-  ( s = (/) -> ( ( D ` s ) ` k ) = ( ( D ` (/) ) ` k ) )
16 15 sumeq1d 
 |-  ( 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 ) ) )
17 prodeq1 
 |-  ( s = (/) -> prod_ t e. s ( ! ` ( c ` t ) ) = prod_ t e. (/) ( ! ` ( c ` t ) ) )
18 17 oveq2d 
 |-  ( s = (/) -> ( ( ! ` k ) / prod_ t e. s ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) )
19 prodeq1 
 |-  ( s = (/) -> prod_ t e. s ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
20 18 19 oveq12d 
 |-  ( 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 ) ) )
21 20 sumeq2sdv 
 |-  ( 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 ) ) )
22 16 21 eqtrd 
 |-  ( 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 ) ) )
23 22 mpteq2dv 
 |-  ( 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 ) ) ) )
24 13 23 eqeq12d 
 |-  ( 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 ) ) ) ) )
25 24 ralbidv 
 |-  ( 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 ) ) ) ) )
26 prodeq1 
 |-  ( s = r -> prod_ t e. s ( ( H ` t ) ` x ) = prod_ t e. r ( ( H ` t ) ` x ) )
27 26 mpteq2dv 
 |-  ( s = r -> ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) )
28 27 oveq2d 
 |-  ( 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 ) ) ) )
29 28 fveq1d 
 |-  ( 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 ) )
30 fveq2 
 |-  ( s = r -> ( D ` s ) = ( D ` r ) )
31 30 fveq1d 
 |-  ( s = r -> ( ( D ` s ) ` k ) = ( ( D ` r ) ` k ) )
32 31 sumeq1d 
 |-  ( 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 ) ) )
33 prodeq1 
 |-  ( s = r -> prod_ t e. s ( ! ` ( c ` t ) ) = prod_ t e. r ( ! ` ( c ` t ) ) )
34 33 oveq2d 
 |-  ( s = r -> ( ( ! ` k ) / prod_ t e. s ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ t e. r ( ! ` ( c ` t ) ) ) )
35 prodeq1 
 |-  ( s = r -> prod_ t e. s ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
36 34 35 oveq12d 
 |-  ( 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 ) ) )
37 36 sumeq2sdv 
 |-  ( 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 ) ) )
38 32 37 eqtrd 
 |-  ( 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 ) ) )
39 38 mpteq2dv 
 |-  ( 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 ) ) ) )
40 29 39 eqeq12d 
 |-  ( 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 ) ) ) ) )
41 40 ralbidv 
 |-  ( 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 ) ) ) ) )
42 prodeq1 
 |-  ( s = ( r u. { z } ) -> prod_ t e. s ( ( H ` t ) ` x ) = prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) )
43 42 mpteq2dv 
 |-  ( 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 ) ) )
44 43 oveq2d 
 |-  ( 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 ) ) ) )
45 44 fveq1d 
 |-  ( 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 ) )
46 fveq2 
 |-  ( s = ( r u. { z } ) -> ( D ` s ) = ( D ` ( r u. { z } ) ) )
47 46 fveq1d 
 |-  ( s = ( r u. { z } ) -> ( ( D ` s ) ` k ) = ( ( D ` ( r u. { z } ) ) ` k ) )
48 47 sumeq1d 
 |-  ( 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 ) ) )
49 prodeq1 
 |-  ( s = ( r u. { z } ) -> prod_ t e. s ( ! ` ( c ` t ) ) = prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) )
50 49 oveq2d 
 |-  ( s = ( r u. { z } ) -> ( ( ! ` k ) / prod_ t e. s ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) )
51 prodeq1 
 |-  ( 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 ) )
52 50 51 oveq12d 
 |-  ( 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 ) ) )
53 52 sumeq2sdv 
 |-  ( 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 ) ) )
54 48 53 eqtrd 
 |-  ( 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 ) ) )
55 54 mpteq2dv 
 |-  ( 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 ) ) ) )
56 45 55 eqeq12d 
 |-  ( 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 ) ) ) ) )
57 56 ralbidv 
 |-  ( 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 ) ) ) ) )
58 prodeq1 
 |-  ( s = T -> prod_ t e. s ( ( H ` t ) ` x ) = prod_ t e. T ( ( H ` t ) ` x ) )
59 58 mpteq2dv 
 |-  ( s = T -> ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) ) )
60 7 a1i 
 |-  ( s = T -> F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) ) )
61 60 eqcomd 
 |-  ( s = T -> ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) ) = F )
62 59 61 eqtrd 
 |-  ( s = T -> ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) = F )
63 62 oveq2d 
 |-  ( s = T -> ( S Dn ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) ) = ( S Dn F ) )
64 63 fveq1d 
 |-  ( s = T -> ( ( S Dn ( x e. X |-> prod_ t e. s ( ( H ` t ) ` x ) ) ) ` k ) = ( ( S Dn F ) ` k ) )
65 fveq2 
 |-  ( s = T -> ( D ` s ) = ( D ` T ) )
66 65 fveq1d 
 |-  ( s = T -> ( ( D ` s ) ` k ) = ( ( D ` T ) ` k ) )
67 66 sumeq1d 
 |-  ( 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 ) ) )
68 prodeq1 
 |-  ( s = T -> prod_ t e. s ( ! ` ( c ` t ) ) = prod_ t e. T ( ! ` ( c ` t ) ) )
69 68 oveq2d 
 |-  ( s = T -> ( ( ! ` k ) / prod_ t e. s ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ t e. T ( ! ` ( c ` t ) ) ) )
70 prodeq1 
 |-  ( s = T -> prod_ t e. s ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
71 69 70 oveq12d 
 |-  ( 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 ) ) )
72 71 sumeq2sdv 
 |-  ( 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 ) ) )
73 67 72 eqtrd 
 |-  ( 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 ) ) )
74 73 mpteq2dv 
 |-  ( 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 ) ) ) )
75 64 74 eqeq12d 
 |-  ( 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 ) ) ) ) )
76 75 ralbidv 
 |-  ( 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 ) ) ) ) )
77 prod0 
 |-  prod_ t e. (/) ( ( H ` t ) ` x ) = 1
78 77 mpteq2i 
 |-  ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) = ( x e. X |-> 1 )
79 78 oveq2i 
 |-  ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) = ( S Dn ( x e. X |-> 1 ) )
80 79 a1i 
 |-  ( k = 0 -> ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) = ( S Dn ( x e. X |-> 1 ) ) )
81 id 
 |-  ( k = 0 -> k = 0 )
82 80 81 fveq12d 
 |-  ( k = 0 -> ( ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) ` k ) = ( ( S Dn ( x e. X |-> 1 ) ) ` 0 ) )
83 82 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) ` k ) = ( ( S Dn ( x e. X |-> 1 ) ) ` 0 ) )
84 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
85 1 84 syl 
 |-  ( ph -> S C_ CC )
86 1cnd 
 |-  ( ( ph /\ x e. X ) -> 1 e. CC )
87 86 fmpttd 
 |-  ( ph -> ( x e. X |-> 1 ) : X --> CC )
88 1re 
 |-  1 e. RR
89 88 rgenw 
 |-  A. x e. X 1 e. RR
90 dmmptg 
 |-  ( A. x e. X 1 e. RR -> dom ( x e. X |-> 1 ) = X )
91 89 90 ax-mp 
 |-  dom ( x e. X |-> 1 ) = X
92 91 a1i 
 |-  ( ph -> dom ( x e. X |-> 1 ) = X )
93 92 feq2d 
 |-  ( ph -> ( ( x e. X |-> 1 ) : dom ( x e. X |-> 1 ) --> CC <-> ( x e. X |-> 1 ) : X --> CC ) )
94 87 93 mpbird 
 |-  ( ph -> ( x e. X |-> 1 ) : dom ( x e. X |-> 1 ) --> CC )
95 restsspw 
 |-  ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S
96 95 2 sselid 
 |-  ( ph -> X e. ~P S )
97 elpwi 
 |-  ( X e. ~P S -> X C_ S )
98 96 97 syl 
 |-  ( ph -> X C_ S )
99 92 98 eqsstrd 
 |-  ( ph -> dom ( x e. X |-> 1 ) C_ S )
100 94 99 jca 
 |-  ( ph -> ( ( x e. X |-> 1 ) : dom ( x e. X |-> 1 ) --> CC /\ dom ( x e. X |-> 1 ) C_ S ) )
101 cnex 
 |-  CC e. _V
102 101 a1i 
 |-  ( ph -> CC e. _V )
103 elpm2g 
 |-  ( ( 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 ) ) )
104 102 1 103 syl2anc 
 |-  ( 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 ) ) )
105 100 104 mpbird 
 |-  ( ph -> ( x e. X |-> 1 ) e. ( CC ^pm S ) )
106 dvn0 
 |-  ( ( S C_ CC /\ ( x e. X |-> 1 ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> 1 ) ) ` 0 ) = ( x e. X |-> 1 ) )
107 85 105 106 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> 1 ) ) ` 0 ) = ( x e. X |-> 1 ) )
108 107 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( ( S Dn ( x e. X |-> 1 ) ) ` 0 ) = ( x e. X |-> 1 ) )
109 fveq2 
 |-  ( k = 0 -> ( ( D ` (/) ) ` k ) = ( ( D ` (/) ) ` 0 ) )
110 109 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( ( D ` (/) ) ` k ) = ( ( D ` (/) ) ` 0 ) )
111 oveq2 
 |-  ( s = (/) -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m (/) ) )
112 elmapfn 
 |-  ( x e. ( ( 0 ... n ) ^m (/) ) -> x Fn (/) )
113 fn0 
 |-  ( x Fn (/) <-> x = (/) )
114 112 113 sylib 
 |-  ( x e. ( ( 0 ... n ) ^m (/) ) -> x = (/) )
115 velsn 
 |-  ( x e. { (/) } <-> x = (/) )
116 114 115 sylibr 
 |-  ( x e. ( ( 0 ... n ) ^m (/) ) -> x e. { (/) } )
117 115 biimpi 
 |-  ( x e. { (/) } -> x = (/) )
118 id 
 |-  ( x = (/) -> x = (/) )
119 f0 
 |-  (/) : (/) --> ( 0 ... n )
120 ovex 
 |-  ( 0 ... n ) e. _V
121 0ex 
 |-  (/) e. _V
122 120 121 elmap 
 |-  ( (/) e. ( ( 0 ... n ) ^m (/) ) <-> (/) : (/) --> ( 0 ... n ) )
123 119 122 mpbir 
 |-  (/) e. ( ( 0 ... n ) ^m (/) )
124 123 a1i 
 |-  ( x = (/) -> (/) e. ( ( 0 ... n ) ^m (/) ) )
125 118 124 eqeltrd 
 |-  ( x = (/) -> x e. ( ( 0 ... n ) ^m (/) ) )
126 117 125 syl 
 |-  ( x e. { (/) } -> x e. ( ( 0 ... n ) ^m (/) ) )
127 116 126 impbii 
 |-  ( x e. ( ( 0 ... n ) ^m (/) ) <-> x e. { (/) } )
128 127 ax-gen 
 |-  A. x ( x e. ( ( 0 ... n ) ^m (/) ) <-> x e. { (/) } )
129 dfcleq 
 |-  ( ( ( 0 ... n ) ^m (/) ) = { (/) } <-> A. x ( x e. ( ( 0 ... n ) ^m (/) ) <-> x e. { (/) } ) )
130 128 129 mpbir 
 |-  ( ( 0 ... n ) ^m (/) ) = { (/) }
131 130 a1i 
 |-  ( s = (/) -> ( ( 0 ... n ) ^m (/) ) = { (/) } )
132 111 131 eqtrd 
 |-  ( s = (/) -> ( ( 0 ... n ) ^m s ) = { (/) } )
133 rabeq 
 |-  ( ( ( 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 } )
134 132 133 syl 
 |-  ( s = (/) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. { (/) } | sum_ t e. s ( c ` t ) = n } )
135 sumeq1 
 |-  ( s = (/) -> sum_ t e. s ( c ` t ) = sum_ t e. (/) ( c ` t ) )
136 135 eqeq1d 
 |-  ( s = (/) -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. (/) ( c ` t ) = n ) )
137 136 rabbidv 
 |-  ( s = (/) -> { c e. { (/) } | sum_ t e. s ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } )
138 134 137 eqtrd 
 |-  ( s = (/) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } )
139 138 mpteq2dv 
 |-  ( 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 } ) )
140 0elpw 
 |-  (/) e. ~P T
141 140 a1i 
 |-  ( ph -> (/) e. ~P T )
142 nn0ex 
 |-  NN0 e. _V
143 142 mptex 
 |-  ( n e. NN0 |-> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } ) e. _V
144 143 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } ) e. _V )
145 8 139 141 144 fvmptd3 
 |-  ( ph -> ( D ` (/) ) = ( n e. NN0 |-> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } ) )
146 eqeq2 
 |-  ( n = 0 -> ( sum_ t e. (/) ( c ` t ) = n <-> sum_ t e. (/) ( c ` t ) = 0 ) )
147 146 rabbidv 
 |-  ( n = 0 -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } )
148 147 adantl 
 |-  ( ( ph /\ n = 0 ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } )
149 0nn0 
 |-  0 e. NN0
150 149 a1i 
 |-  ( ph -> 0 e. NN0 )
151 p0ex 
 |-  { (/) } e. _V
152 151 rabex 
 |-  { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } e. _V
153 152 a1i 
 |-  ( ph -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } e. _V )
154 145 148 150 153 fvmptd 
 |-  ( ph -> ( ( D ` (/) ) ` 0 ) = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } )
155 154 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( ( D ` (/) ) ` 0 ) = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } )
156 snidg 
 |-  ( (/) e. _V -> (/) e. { (/) } )
157 121 156 ax-mp 
 |-  (/) e. { (/) }
158 eqid 
 |-  0 = 0
159 157 158 pm3.2i 
 |-  ( (/) e. { (/) } /\ 0 = 0 )
160 sum0 
 |-  sum_ t e. (/) ( c ` t ) = 0
161 160 a1i 
 |-  ( c = (/) -> sum_ t e. (/) ( c ` t ) = 0 )
162 161 eqeq1d 
 |-  ( c = (/) -> ( sum_ t e. (/) ( c ` t ) = 0 <-> 0 = 0 ) )
163 162 elrab 
 |-  ( (/) e. { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } <-> ( (/) e. { (/) } /\ 0 = 0 ) )
164 159 163 mpbir 
 |-  (/) e. { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 }
165 164 n0ii 
 |-  -. { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = (/)
166 eqid 
 |-  { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 }
167 rabrsn 
 |-  ( { 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 } = { (/) } ) )
168 166 167 ax-mp 
 |-  ( { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = (/) \/ { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = { (/) } )
169 165 168 mtpor 
 |-  { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = { (/) }
170 169 a1i 
 |-  ( ( ph /\ k = 0 ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = { (/) } )
171 iftrue 
 |-  ( k = 0 -> if ( k = 0 , { (/) } , (/) ) = { (/) } )
172 171 adantl 
 |-  ( ( ph /\ k = 0 ) -> if ( k = 0 , { (/) } , (/) ) = { (/) } )
173 170 172 eqtr4d 
 |-  ( ( ph /\ k = 0 ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = 0 } = if ( k = 0 , { (/) } , (/) ) )
174 110 155 173 3eqtrd 
 |-  ( ( ph /\ k = 0 ) -> ( ( D ` (/) ) ` k ) = if ( k = 0 , { (/) } , (/) ) )
175 174 172 eqtrd 
 |-  ( ( ph /\ k = 0 ) -> ( ( D ` (/) ) ` k ) = { (/) } )
176 175 sumeq1d 
 |-  ( ( 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 ) ) )
177 fveq2 
 |-  ( k = 0 -> ( ! ` k ) = ( ! ` 0 ) )
178 fac0 
 |-  ( ! ` 0 ) = 1
179 178 a1i 
 |-  ( k = 0 -> ( ! ` 0 ) = 1 )
180 177 179 eqtrd 
 |-  ( k = 0 -> ( ! ` k ) = 1 )
181 180 oveq1d 
 |-  ( k = 0 -> ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) = ( 1 / prod_ t e. (/) ( ! ` ( c ` t ) ) ) )
182 prod0 
 |-  prod_ t e. (/) ( ! ` ( c ` t ) ) = 1
183 182 oveq2i 
 |-  ( 1 / prod_ t e. (/) ( ! ` ( c ` t ) ) ) = ( 1 / 1 )
184 1div1e1 
 |-  ( 1 / 1 ) = 1
185 183 184 eqtri 
 |-  ( 1 / prod_ t e. (/) ( ! ` ( c ` t ) ) ) = 1
186 181 185 eqtrdi 
 |-  ( k = 0 -> ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) = 1 )
187 prod0 
 |-  prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = 1
188 187 a1i 
 |-  ( k = 0 -> prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = 1 )
189 186 188 oveq12d 
 |-  ( k = 0 -> ( ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) x. prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = ( 1 x. 1 ) )
190 189 ad2antlr 
 |-  ( ( ( 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 ) )
191 1t1e1 
 |-  ( 1 x. 1 ) = 1
192 191 a1i 
 |-  ( ( ( ph /\ k = 0 ) /\ c e. { (/) } ) -> ( 1 x. 1 ) = 1 )
193 190 192 eqtrd 
 |-  ( ( ( ph /\ k = 0 ) /\ c e. { (/) } ) -> ( ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) x. prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = 1 )
194 193 sumeq2dv 
 |-  ( ( 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 )
195 ax-1cn 
 |-  1 e. CC
196 eqidd 
 |-  ( c = (/) -> 1 = 1 )
197 196 sumsn 
 |-  ( ( (/) e. _V /\ 1 e. CC ) -> sum_ c e. { (/) } 1 = 1 )
198 121 195 197 mp2an 
 |-  sum_ c e. { (/) } 1 = 1
199 198 a1i 
 |-  ( ( ph /\ k = 0 ) -> sum_ c e. { (/) } 1 = 1 )
200 176 194 199 3eqtrd 
 |-  ( ( 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 )
201 200 mpteq2dv 
 |-  ( ( 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 ) )
202 201 eqcomd 
 |-  ( ( 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 ) ) ) )
203 83 108 202 3eqtrd 
 |-  ( ( 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 ) ) ) )
204 203 a1d 
 |-  ( ( 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 ) ) ) ) )
205 79 fveq1i 
 |-  ( ( S Dn ( x e. X |-> prod_ t e. (/) ( ( H ` t ) ` x ) ) ) ` k ) = ( ( S Dn ( x e. X |-> 1 ) ) ` k )
206 205 a1i 
 |-  ( ( ( 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 ) )
207 1 adantr 
 |-  ( ( ph /\ -. k = 0 ) -> S e. { RR , CC } )
208 207 adantr 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> S e. { RR , CC } )
209 2 adantr 
 |-  ( ( ph /\ -. k = 0 ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
210 209 adantr 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
211 195 a1i 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> 1 e. CC )
212 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
213 212 adantl 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... N ) ) -> k e. NN0 )
214 neqne 
 |-  ( -. k = 0 -> k =/= 0 )
215 214 adantr 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... N ) ) -> k =/= 0 )
216 213 215 jca 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... N ) ) -> ( k e. NN0 /\ k =/= 0 ) )
217 elnnne0 
 |-  ( k e. NN <-> ( k e. NN0 /\ k =/= 0 ) )
218 216 217 sylibr 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... N ) ) -> k e. NN )
219 218 adantll 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> k e. NN )
220 208 210 211 219 dvnmptconst 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( x e. X |-> 1 ) ) ` k ) = ( x e. X |-> 0 ) )
221 145 ad2antrr 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> ( D ` (/) ) = ( n e. NN0 |-> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } ) )
222 eqeq2 
 |-  ( n = k -> ( sum_ t e. (/) ( c ` t ) = n <-> sum_ t e. (/) ( c ` t ) = k ) )
223 222 rabbidv 
 |-  ( n = k -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = k } )
224 223 adantl 
 |-  ( ( -. k = 0 /\ n = k ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = { c e. { (/) } | sum_ t e. (/) ( c ` t ) = k } )
225 eqidd 
 |-  ( sum_ t e. (/) ( c ` t ) = k -> k = k )
226 id 
 |-  ( sum_ t e. (/) ( c ` t ) = k -> sum_ t e. (/) ( c ` t ) = k )
227 226 eqcomd 
 |-  ( sum_ t e. (/) ( c ` t ) = k -> k = sum_ t e. (/) ( c ` t ) )
228 160 a1i 
 |-  ( sum_ t e. (/) ( c ` t ) = k -> sum_ t e. (/) ( c ` t ) = 0 )
229 225 227 228 3eqtrd 
 |-  ( sum_ t e. (/) ( c ` t ) = k -> k = 0 )
230 229 adantl 
 |-  ( ( c e. { (/) } /\ sum_ t e. (/) ( c ` t ) = k ) -> k = 0 )
231 230 adantll 
 |-  ( ( ( -. k = 0 /\ c e. { (/) } ) /\ sum_ t e. (/) ( c ` t ) = k ) -> k = 0 )
232 simpll 
 |-  ( ( ( -. k = 0 /\ c e. { (/) } ) /\ sum_ t e. (/) ( c ` t ) = k ) -> -. k = 0 )
233 231 232 pm2.65da 
 |-  ( ( -. k = 0 /\ c e. { (/) } ) -> -. sum_ t e. (/) ( c ` t ) = k )
234 233 ralrimiva 
 |-  ( -. k = 0 -> A. c e. { (/) } -. sum_ t e. (/) ( c ` t ) = k )
235 rabeq0 
 |-  ( { c e. { (/) } | sum_ t e. (/) ( c ` t ) = k } = (/) <-> A. c e. { (/) } -. sum_ t e. (/) ( c ` t ) = k )
236 234 235 sylibr 
 |-  ( -. k = 0 -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = k } = (/) )
237 236 adantr 
 |-  ( ( -. k = 0 /\ n = k ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = k } = (/) )
238 224 237 eqtrd 
 |-  ( ( -. k = 0 /\ n = k ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = (/) )
239 238 adantll 
 |-  ( ( ( ph /\ -. k = 0 ) /\ n = k ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = (/) )
240 239 adantlr 
 |-  ( ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) /\ n = k ) -> { c e. { (/) } | sum_ t e. (/) ( c ` t ) = n } = (/) )
241 212 adantl 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
242 121 a1i 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> (/) e. _V )
243 221 240 241 242 fvmptd 
 |-  ( ( ( ph /\ -. k = 0 ) /\ k e. ( 0 ... N ) ) -> ( ( D ` (/) ) ` k ) = (/) )
244 243 sumeq1d 
 |-  ( ( ( 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 ) ) )
245 sum0 
 |-  sum_ c e. (/) ( ( ( ! ` k ) / prod_ t e. (/) ( ! ` ( c ` t ) ) ) x. prod_ t e. (/) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = 0
246 245 a1i 
 |-  ( ( ( 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 )
247 244 246 eqtr2d 
 |-  ( ( ( 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 ) ) )
248 247 mpteq2dv 
 |-  ( ( ( 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 ) ) ) )
249 206 220 248 3eqtrd 
 |-  ( ( ( 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 ) ) ) )
250 249 ex 
 |-  ( ( 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 ) ) ) ) )
251 204 250 pm2.61dan 
 |-  ( 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 ) ) ) ) )
252 251 ralrimiv 
 |-  ( 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 ) ) ) )
253 simpll 
 |-  ( ( ( ( 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 ) ) ) )
254 fveq2 
 |-  ( x = y -> ( ( H ` t ) ` x ) = ( ( H ` t ) ` y ) )
255 254 prodeq2ad 
 |-  ( x = y -> prod_ t e. r ( ( H ` t ) ` x ) = prod_ t e. r ( ( H ` t ) ` y ) )
256 fveq2 
 |-  ( t = u -> ( H ` t ) = ( H ` u ) )
257 256 fveq1d 
 |-  ( t = u -> ( ( H ` t ) ` y ) = ( ( H ` u ) ` y ) )
258 257 cbvprodv 
 |-  prod_ t e. r ( ( H ` t ) ` y ) = prod_ u e. r ( ( H ` u ) ` y )
259 258 a1i 
 |-  ( x = y -> prod_ t e. r ( ( H ` t ) ` y ) = prod_ u e. r ( ( H ` u ) ` y ) )
260 255 259 eqtrd 
 |-  ( x = y -> prod_ t e. r ( ( H ` t ) ` x ) = prod_ u e. r ( ( H ` u ) ` y ) )
261 260 cbvmptv 
 |-  ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) = ( y e. X |-> prod_ u e. r ( ( H ` u ) ` y ) )
262 261 oveq2i 
 |-  ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) = ( S Dn ( y e. X |-> prod_ u e. r ( ( H ` u ) ` y ) ) )
263 262 fveq1i 
 |-  ( ( 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 )
264 fveq2 
 |-  ( t = u -> ( c ` t ) = ( c ` u ) )
265 264 fveq2d 
 |-  ( t = u -> ( ! ` ( c ` t ) ) = ( ! ` ( c ` u ) ) )
266 265 cbvprodv 
 |-  prod_ t e. r ( ! ` ( c ` t ) ) = prod_ u e. r ( ! ` ( c ` u ) )
267 266 oveq2i 
 |-  ( ( ! ` k ) / prod_ t e. r ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ u e. r ( ! ` ( c ` u ) ) )
268 267 a1i 
 |-  ( x = y -> ( ( ! ` k ) / prod_ t e. r ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ u e. r ( ! ` ( c ` u ) ) ) )
269 fveq2 
 |-  ( x = y -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` y ) )
270 269 prodeq2ad 
 |-  ( x = y -> prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` y ) )
271 256 oveq2d 
 |-  ( t = u -> ( S Dn ( H ` t ) ) = ( S Dn ( H ` u ) ) )
272 271 264 fveq12d 
 |-  ( t = u -> ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) = ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) )
273 272 fveq1d 
 |-  ( t = u -> ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` y ) = ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y ) )
274 273 cbvprodv 
 |-  prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` y ) = prod_ u e. r ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y )
275 274 a1i 
 |-  ( x = y -> prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` y ) = prod_ u e. r ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y ) )
276 270 275 eqtrd 
 |-  ( x = y -> prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) = prod_ u e. r ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y ) )
277 268 276 oveq12d 
 |-  ( 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 ) ) )
278 277 sumeq2sdv 
 |-  ( 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 ) ) )
279 fveq1 
 |-  ( c = d -> ( c ` u ) = ( d ` u ) )
280 279 fveq2d 
 |-  ( c = d -> ( ! ` ( c ` u ) ) = ( ! ` ( d ` u ) ) )
281 280 prodeq2ad 
 |-  ( c = d -> prod_ u e. r ( ! ` ( c ` u ) ) = prod_ u e. r ( ! ` ( d ` u ) ) )
282 281 oveq2d 
 |-  ( c = d -> ( ( ! ` k ) / prod_ u e. r ( ! ` ( c ` u ) ) ) = ( ( ! ` k ) / prod_ u e. r ( ! ` ( d ` u ) ) ) )
283 279 fveq2d 
 |-  ( c = d -> ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) = ( ( S Dn ( H ` u ) ) ` ( d ` u ) ) )
284 283 fveq1d 
 |-  ( c = d -> ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y ) = ( ( ( S Dn ( H ` u ) ) ` ( d ` u ) ) ` y ) )
285 284 prodeq2ad 
 |-  ( c = d -> prod_ u e. r ( ( ( S Dn ( H ` u ) ) ` ( c ` u ) ) ` y ) = prod_ u e. r ( ( ( S Dn ( H ` u ) ) ` ( d ` u ) ) ` y ) )
286 282 285 oveq12d 
 |-  ( 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 ) ) )
287 286 cbvsumv 
 |-  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 ) )
288 287 a1i 
 |-  ( 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 ) ) )
289 278 288 eqtrd 
 |-  ( 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 ) ) )
290 289 cbvmptv 
 |-  ( 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 ) ) )
291 263 290 eqeq12i 
 |-  ( ( ( 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 ) ) ) )
292 291 ralbii 
 |-  ( 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 ) ) ) )
293 292 biimpi 
 |-  ( 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 ) ) ) )
294 293 ad2antlr 
 |-  ( ( ( ( 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 ) ) ) )
295 simpr 
 |-  ( ( ( ( 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 ) )
296 1 ad3antrrr 
 |-  ( ( ( ( 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 } )
297 2 ad3antrrr 
 |-  ( ( ( ( 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 ` CCfld ) |`t S ) )
298 3 ad3antrrr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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. T ) -> ph )
300 simpr 
 |-  ( ( ( ( ( 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. T ) -> t e. T )
301 299 300 4 syl2anc 
 |-  ( ( ( ( ( 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. T ) -> ( H ` t ) : X --> CC )
302 5 ad3antrrr 
 |-  ( ( ( ( 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 ) ) -> N e. NN0 )
303 simplll 
 |-  ( ( ( ( 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 ) ) -> ph )
304 303 3ad2ant1 
 |-  ( ( ( ( ( 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. T /\ h e. ( 0 ... N ) ) -> ph )
305 simp2 
 |-  ( ( ( ( ( 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. T /\ h e. ( 0 ... N ) ) -> t e. T )
306 simp3 
 |-  ( ( ( ( ( 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. T /\ h e. ( 0 ... N ) ) -> h e. ( 0 ... N ) )
307 eleq1w 
 |-  ( j = h -> ( j e. ( 0 ... N ) <-> h e. ( 0 ... N ) ) )
308 307 3anbi3d 
 |-  ( j = h -> ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. T /\ h e. ( 0 ... N ) ) ) )
309 fveq2 
 |-  ( j = h -> ( ( S Dn ( H ` t ) ) ` j ) = ( ( S Dn ( H ` t ) ) ` h ) )
310 309 feq1d 
 |-  ( j = h -> ( ( ( S Dn ( H ` t ) ) ` j ) : X --> CC <-> ( ( S Dn ( H ` t ) ) ` h ) : X --> CC ) )
311 308 310 imbi12d 
 |-  ( j = h -> ( ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC ) <-> ( ( ph /\ t e. T /\ h e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` h ) : X --> CC ) ) )
312 311 6 chvarvv 
 |-  ( ( ph /\ t e. T /\ h e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` h ) : X --> CC )
313 304 305 306 312 syl3anc 
 |-  ( ( ( ( ( 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. T /\ h e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` h ) : X --> CC )
314 simprl 
 |-  ( ( ph /\ ( r C_ T /\ z e. ( T \ r ) ) ) -> r C_ T )
315 314 ad2antrr 
 |-  ( ( ( ( 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 ) ) -> r C_ T )
316 simprr 
 |-  ( ( ph /\ ( r C_ T /\ z e. ( T \ r ) ) ) -> z e. ( T \ r ) )
317 316 ad2antrr 
 |-  ( ( ( ( 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 ) ) -> z e. ( T \ r ) )
318 262 eqcomi 
 |-  ( S Dn ( y e. X |-> prod_ u e. r ( ( H ` u ) ` y ) ) ) = ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) )
319 318 a1i 
 |-  ( k = l -> ( S Dn ( y e. X |-> prod_ u e. r ( ( H ` u ) ` y ) ) ) = ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) )
320 id 
 |-  ( k = l -> k = l )
321 319 320 fveq12d 
 |-  ( k = l -> ( ( S Dn ( y e. X |-> prod_ u e. r ( ( H ` u ) ` y ) ) ) ` k ) = ( ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) ` l ) )
322 290 eqcomi 
 |-  ( 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 ) ) ) = ( 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 ) ) )
323 322 a1i 
 |-  ( k = l -> ( 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 ) ) ) = ( 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 ) ) ) )
324 fveq2 
 |-  ( k = l -> ( ! ` k ) = ( ! ` l ) )
325 324 oveq1d 
 |-  ( k = l -> ( ( ! ` k ) / prod_ t e. r ( ! ` ( c ` t ) ) ) = ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) )
326 325 oveq1d 
 |-  ( k = l -> ( ( ( ! ` k ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
327 326 sumeq2sdv 
 |-  ( k = l -> 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 ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
328 fveq2 
 |-  ( k = l -> ( ( D ` r ) ` k ) = ( ( D ` r ) ` l ) )
329 328 sumeq1d 
 |-  ( k = l -> sum_ c e. ( ( D ` r ) ` k ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
330 327 329 eqtrd 
 |-  ( k = l -> 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 ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
331 330 mpteq2dv 
 |-  ( k = l -> ( 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 ) ) ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
332 323 331 eqtrd 
 |-  ( k = l -> ( 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 ) ) ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
333 321 332 eqeq12d 
 |-  ( k = l -> ( ( ( 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 ) ) ) <-> ( ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) ` l ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ) )
334 333 cbvralvw 
 |-  ( 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 ) ) ) <-> A. l e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) ` l ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
335 334 biimpi 
 |-  ( 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 ) ) ) -> A. l e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) ` l ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
336 335 ad2antlr 
 |-  ( ( ( ( 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 ) ) -> A. l e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. r ( ( H ` t ) ` x ) ) ) ` l ) = ( x e. X |-> sum_ c e. ( ( D ` r ) ` l ) ( ( ( ! ` l ) / prod_ t e. r ( ! ` ( c ` t ) ) ) x. prod_ t e. r ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
337 simpr 
 |-  ( ( ( ( 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 ) ) -> j e. ( 0 ... N ) )
338 fveq1 
 |-  ( d = c -> ( d ` z ) = ( c ` z ) )
339 338 oveq2d 
 |-  ( d = c -> ( j - ( d ` z ) ) = ( j - ( c ` z ) ) )
340 reseq1 
 |-  ( d = c -> ( d |` r ) = ( c |` r ) )
341 339 340 opeq12d 
 |-  ( d = c -> <. ( j - ( d ` z ) ) , ( d |` r ) >. = <. ( j - ( c ` z ) ) , ( c |` r ) >. )
342 341 cbvmptv 
 |-  ( d e. ( ( D ` ( r u. { z } ) ) ` j ) |-> <. ( j - ( d ` z ) ) , ( d |` r ) >. ) = ( c e. ( ( D ` ( r u. { z } ) ) ` j ) |-> <. ( j - ( c ` z ) ) , ( c |` r ) >. )
343 296 297 298 301 302 313 8 315 317 336 337 342 dvnprodlem2 
 |-  ( ( ( ( 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 Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
344 253 294 295 343 syl21anc 
 |-  ( ( ( ( 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 ) ) -> ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
345 344 ralrimiva 
 |-  ( ( ( 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 ) ) ) ) -> A. j e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
346 fveq2 
 |-  ( j = k -> ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` k ) )
347 fveq2 
 |-  ( j = k -> ( ! ` j ) = ( ! ` k ) )
348 347 oveq1d 
 |-  ( j = k -> ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) = ( ( ! ` k ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) )
349 348 oveq1d 
 |-  ( j = k -> ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( 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 ) ) )
350 349 sumeq2sdv 
 |-  ( j = k -> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` k ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
351 fveq2 
 |-  ( j = k -> ( ( D ` ( r u. { z } ) ) ` j ) = ( ( D ` ( r u. { z } ) ) ` k ) )
352 351 sumeq1d 
 |-  ( j = k -> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` k ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( 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 ) ) )
353 350 352 eqtrd 
 |-  ( j = k -> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = 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 ) ) )
354 353 mpteq2dv 
 |-  ( j = k -> ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) = ( 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 ) ) ) )
355 346 354 eqeq12d 
 |-  ( j = k -> ( ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) <-> ( ( 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 ) ) ) ) )
356 355 cbvralvw 
 |-  ( A. j e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. ( r u. { z } ) ( ( H ` t ) ` x ) ) ) ` j ) = ( x e. X |-> sum_ c e. ( ( D ` ( r u. { z } ) ) ` j ) ( ( ( ! ` j ) / prod_ t e. ( r u. { z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( r u. { z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) <-> 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 ) ) ) )
357 345 356 sylib 
 |-  ( ( ( 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 ) ) ) ) -> 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 ) ) ) )
358 357 ex 
 |-  ( ( 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 ) ) ) -> 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 ) ) ) ) )
359 25 41 57 76 252 358 3 findcard2d 
 |-  ( ph -> 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 ) ) ) )
360 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
361 5 360 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
362 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
363 361 362 syl 
 |-  ( ph -> N e. ( 0 ... N ) )
364 fveq2 
 |-  ( k = N -> ( ( S Dn F ) ` k ) = ( ( S Dn F ) ` N ) )
365 fveq2 
 |-  ( k = N -> ( ( D ` T ) ` k ) = ( ( D ` T ) ` N ) )
366 365 sumeq1d 
 |-  ( k = N -> 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 ) ) = sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` k ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
367 fveq2 
 |-  ( k = N -> ( ! ` k ) = ( ! ` N ) )
368 367 oveq1d 
 |-  ( k = N -> ( ( ! ` k ) / prod_ t e. T ( ! ` ( c ` t ) ) ) = ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) )
369 368 oveq1d 
 |-  ( k = N -> ( ( ( ! ` k ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
370 369 sumeq2sdv 
 |-  ( k = N -> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` k ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) = sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
371 366 370 eqtrd 
 |-  ( k = N -> 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 ) ) = sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
372 371 mpteq2dv 
 |-  ( k = N -> ( 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 ) ) ) = ( x e. X |-> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
373 364 372 eqeq12d 
 |-  ( k = 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 ) ) ) <-> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) ) )
374 373 rspccva 
 |-  ( ( 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 ) ) ) /\ N e. ( 0 ... N ) ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
375 359 363 374 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
376 oveq2 
 |-  ( s = T -> ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m T ) )
377 rabeq 
 |-  ( ( ( 0 ... n ) ^m s ) = ( ( 0 ... n ) ^m T ) -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. s ( c ` t ) = n } )
378 376 377 syl 
 |-  ( s = T -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. s ( c ` t ) = n } )
379 sumeq1 
 |-  ( s = T -> sum_ t e. s ( c ` t ) = sum_ t e. T ( c ` t ) )
380 379 eqeq1d 
 |-  ( s = T -> ( sum_ t e. s ( c ` t ) = n <-> sum_ t e. T ( c ` t ) = n ) )
381 380 rabbidv 
 |-  ( s = T -> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )
382 378 381 eqtrd 
 |-  ( s = T -> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } = { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )
383 382 mpteq2dv 
 |-  ( s = T -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) )
384 pwidg 
 |-  ( T e. Fin -> T e. ~P T )
385 3 384 syl 
 |-  ( ph -> T e. ~P T )
386 142 mptex 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) e. _V
387 386 a1i 
 |-  ( ph -> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) e. _V )
388 8 383 385 387 fvmptd3 
 |-  ( ph -> ( D ` T ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) )
389 9 a1i 
 |-  ( ph -> C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) )
390 388 389 eqtr4d 
 |-  ( ph -> ( D ` T ) = C )
391 390 fveq1d 
 |-  ( ph -> ( ( D ` T ) ` N ) = ( C ` N ) )
392 391 sumeq1d 
 |-  ( ph -> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` 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 ) ) )
393 392 mpteq2dv 
 |-  ( ph -> ( x e. X |-> sum_ c e. ( ( D ` T ) ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) = ( 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 ) ) ) )
394 375 393 eqtrd 
 |-  ( 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 ) ) ) )