MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-psd Unicode version

Definition df-psd 16120
Description: Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
df-psd  |- mPSDer  =  ( i  e.  _V , 
r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  ( Base `  ( i mPwSer  r ) )  |->  ( k  e. 
{ h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin } 
|->  ( ( ( k `
 x )  +  1 ) (.g `  r
) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) ) ) ) )
Distinct variable group:    f, h, i, k, r, x, y

Detailed syntax breakdown of Definition df-psd
StepHypRef Expression
1 cpsd 16109 . 2  class mPSDer
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vx . . . 4  set  x
62cv 1631 . . . 4  class  i
7 vf . . . . 5  set  f
83cv 1631 . . . . . . 7  class  r
9 cmps 16103 . . . . . . 7  class mPwSer
106, 8, 9co 5874 . . . . . 6  class  ( i mPwSer 
r )
11 cbs 13164 . . . . . 6  class  Base
1210, 11cfv 5271 . . . . 5  class  ( Base `  ( i mPwSer  r ) )
13 vk . . . . . 6  set  k
14 vh . . . . . . . . . . 11  set  h
1514cv 1631 . . . . . . . . . 10  class  h
1615ccnv 4704 . . . . . . . . 9  class  `' h
17 cn 9762 . . . . . . . . 9  class  NN
1816, 17cima 4708 . . . . . . . 8  class  ( `' h " NN )
19 cfn 6879 . . . . . . . 8  class  Fin
2018, 19wcel 1696 . . . . . . 7  wff  ( `' h " NN )  e.  Fin
21 cn0 9981 . . . . . . . 8  class  NN0
22 cmap 6788 . . . . . . . 8  class  ^m
2321, 6, 22co 5874 . . . . . . 7  class  ( NN0 
^m  i )
2420, 14, 23crab 2560 . . . . . 6  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
255cv 1631 . . . . . . . . 9  class  x
2613cv 1631 . . . . . . . . 9  class  k
2725, 26cfv 5271 . . . . . . . 8  class  ( k `
 x )
28 c1 8754 . . . . . . . 8  class  1
29 caddc 8756 . . . . . . . 8  class  +
3027, 28, 29co 5874 . . . . . . 7  class  ( ( k `  x )  +  1 )
31 vy . . . . . . . . . 10  set  y
3231, 5weq 1633 . . . . . . . . . . 11  wff  y  =  x
33 cc0 8753 . . . . . . . . . . 11  class  0
3432, 28, 33cif 3578 . . . . . . . . . 10  class  if ( y  =  x ,  1 ,  0 )
3531, 6, 34cmpt 4093 . . . . . . . . 9  class  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) )
3629cof 6092 . . . . . . . . 9  class  o F  +
3726, 35, 36co 5874 . . . . . . . 8  class  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) )
387cv 1631 . . . . . . . 8  class  f
3937, 38cfv 5271 . . . . . . 7  class  ( f `
 ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) )
40 cmg 14382 . . . . . . . 8  class .g
418, 40cfv 5271 . . . . . . 7  class  (.g `  r
)
4230, 39, 41co 5874 . . . . . 6  class  ( ( ( k `  x
)  +  1 ) (.g `  r ) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) )
4313, 24, 42cmpt 4093 . . . . 5  class  ( k  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  ( ( ( k `  x )  +  1 ) (.g `  r ) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) )
447, 12, 43cmpt 4093 . . . 4  class  ( f  e.  ( Base `  (
i mPwSer  r ) )  |->  ( k  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  ( ( ( k `  x )  +  1 ) (.g `  r ) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) ) )
455, 6, 44cmpt 4093 . . 3  class  ( x  e.  i  |->  ( f  e.  ( Base `  (
i mPwSer  r ) )  |->  ( k  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  ( ( ( k `  x )  +  1 ) (.g `  r ) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) ) ) )
462, 3, 4, 4, 45cmpt2 5876 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  ( Base `  (
i mPwSer  r ) )  |->  ( k  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  ( ( ( k `  x )  +  1 ) (.g `  r ) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) ) ) ) )
471, 46wceq 1632 1  wff mPSDer  =  ( i  e.  _V , 
r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  ( Base `  ( i mPwSer  r ) )  |->  ( k  e. 
{ h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin } 
|->  ( ( ( k `
 x )  +  1 ) (.g `  r
) ( f `  ( k  o F  +  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator