Metamath Proof Explorer

Theorem dvnprod

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

Ref Expression
Hypotheses dvnprod.s 
|- ( ph -> S e. { RR , CC } )
dvnprod.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
dvnprod.t 
|- ( ph -> T e. Fin )
dvnprod.h 
|- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
dvnprod.n 
|- ( ph -> N e. NN0 )
dvnprod.dvnh 
|- ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC )
dvnprod.f 
|- F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) )
dvnprod.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )
Assertion dvnprod 
|- ( 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 dvnprod.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnprod.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvnprod.t 
 |-  ( ph -> T e. Fin )
4 dvnprod.h 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )
5 dvnprod.n 
 |-  ( ph -> N e. NN0 )
6 dvnprod.dvnh 
 |-  ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC )
7 dvnprod.f 
 |-  F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) )
8 dvnprod.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )
9 fveq2 
 |-  ( u = t -> ( d ` u ) = ( d ` t ) )
10 9 cbvsumv 
 |-  sum_ u e. r ( d ` u ) = sum_ t e. r ( d ` t )
11 10 eqeq1i 
 |-  ( sum_ u e. r ( d ` u ) = m <-> sum_ t e. r ( d ` t ) = m )
12 11 rabbii 
 |-  { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } = { d e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( d ` t ) = m }
13 fveq1 
 |-  ( d = e -> ( d ` t ) = ( e ` t ) )
14 13 sumeq2sdv 
 |-  ( d = e -> sum_ t e. r ( d ` t ) = sum_ t e. r ( e ` t ) )
15 14 eqeq1d 
 |-  ( d = e -> ( sum_ t e. r ( d ` t ) = m <-> sum_ t e. r ( e ` t ) = m ) )
16 15 cbvrabv 
 |-  { d e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( d ` t ) = m } = { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m }
17 12 16 eqtri 
 |-  { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } = { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m }
18 17 mpteq2i 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } ) = ( m e. NN0 |-> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m } )
19 eqeq2 
 |-  ( m = n -> ( sum_ t e. r ( e ` t ) = m <-> sum_ t e. r ( e ` t ) = n ) )
20 19 rabbidv 
 |-  ( m = n -> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m } = { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
21 oveq2 
 |-  ( m = n -> ( 0 ... m ) = ( 0 ... n ) )
22 21 oveq1d 
 |-  ( m = n -> ( ( 0 ... m ) ^m r ) = ( ( 0 ... n ) ^m r ) )
23 rabeq 
 |-  ( ( ( 0 ... m ) ^m r ) = ( ( 0 ... n ) ^m r ) -> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
24 22 23 syl 
 |-  ( m = n -> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
25 20 24 eqtrd 
 |-  ( m = n -> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m } = { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
26 25 cbvmptv 
 |-  ( m e. NN0 |-> { e e. ( ( 0 ... m ) ^m r ) | sum_ t e. r ( e ` t ) = m } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
27 18 26 eqtri 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } )
28 27 mpteq2i 
 |-  ( r e. ~P T |-> ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } ) ) = ( r e. ~P T |-> ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } ) )
29 sumeq1 
 |-  ( r = s -> sum_ t e. r ( e ` t ) = sum_ t e. s ( e ` t ) )
30 29 eqeq1d 
 |-  ( r = s -> ( sum_ t e. r ( e ` t ) = n <-> sum_ t e. s ( e ` t ) = n ) )
31 30 rabbidv 
 |-  ( r = s -> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. s ( e ` t ) = n } )
32 oveq2 
 |-  ( r = s -> ( ( 0 ... n ) ^m r ) = ( ( 0 ... n ) ^m s ) )
33 rabeq 
 |-  ( ( ( 0 ... n ) ^m r ) = ( ( 0 ... n ) ^m s ) -> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. s ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } )
34 32 33 syl 
 |-  ( r = s -> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. s ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } )
35 31 34 eqtrd 
 |-  ( r = s -> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } = { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } )
36 35 mpteq2dv 
 |-  ( r = s -> ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } ) )
37 36 cbvmptv 
 |-  ( r e. ~P T |-> ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m r ) | sum_ t e. r ( e ` t ) = n } ) ) = ( s e. ~P T |-> ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } ) )
38 28 37 eqtri 
 |-  ( r e. ~P T |-> ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m r ) | sum_ u e. r ( d ` u ) = m } ) ) = ( s e. ~P T |-> ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( e ` t ) = n } ) )
39 fveq1 
 |-  ( c = e -> ( c ` t ) = ( e ` t ) )
40 39 sumeq2sdv 
 |-  ( c = e -> sum_ t e. T ( c ` t ) = sum_ t e. T ( e ` t ) )
41 40 eqeq1d 
 |-  ( c = e -> ( sum_ t e. T ( c ` t ) = n <-> sum_ t e. T ( e ` t ) = n ) )
42 41 cbvrabv 
 |-  { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } = { e e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( e ` t ) = n }
43 42 mpteq2i 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( e ` t ) = n } )
44 8 43 eqtri 
 |-  C = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( e ` t ) = n } )
45 1 2 3 4 5 6 7 38 44 dvnprodlem3 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ e e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` t ) ) ` x ) ) ) )
46 fveq1 
 |-  ( e = c -> ( e ` t ) = ( c ` t ) )
47 46 fveq2d 
 |-  ( e = c -> ( ! ` ( e ` t ) ) = ( ! ` ( c ` t ) ) )
48 47 prodeq2ad 
 |-  ( e = c -> prod_ t e. T ( ! ` ( e ` t ) ) = prod_ t e. T ( ! ` ( c ` t ) ) )
49 48 oveq2d 
 |-  ( e = c -> ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) = ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) )
50 46 fveq2d 
 |-  ( e = c -> ( ( S Dn ( H ` t ) ) ` ( e ` t ) ) = ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) )
51 50 fveq1d 
 |-  ( e = c -> ( ( ( S Dn ( H ` t ) ) ` ( e ` t ) ) ` x ) = ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
52 51 prodeq2ad 
 |-  ( e = c -> prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` t ) ) ` x ) = prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) )
53 49 52 oveq12d 
 |-  ( e = c -> ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` t ) ) ` x ) ) = ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) )
54 53 cbvsumv 
 |-  sum_ e e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` 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 ) )
55 eqid 
 |-  sum_ c e. ( C ` 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 ) )
56 54 55 eqtri 
 |-  sum_ e e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` 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 ) )
57 56 mpteq2i 
 |-  ( x e. X |-> sum_ e e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` 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 ) ) )
58 57 a1i 
 |-  ( ph -> ( x e. X |-> sum_ e e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( e ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( e ` 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 ) ) ) )
59 45 58 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 ) ) ) )