Metamath Proof Explorer

Definition df-psd

Description: Define the differentiation operation on multivariate polynomials. ( ( ( I mPSDer R )X )F ) is the partial derivative of the polynomial F with respect to X . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 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 oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsd 
 |-  mPSDer
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vx 
 |-  x
5 1 cv 
 |-  i
6 vf 
 |-  f
7 cbs 
 |-  Base
8 cmps 
 |-  mPwSer
9 3 cv 
 |-  r
10 5 9 8 co 
 |-  ( i mPwSer r )
11 10 7 cfv 
 |-  ( Base ` ( i mPwSer r ) )
12 vk 
 |-  k
13 vh 
 |-  h
14 cn0 
 |-  NN0
15 cmap 
 |-  ^m
16 14 5 15 co 
 |-  ( NN0 ^m i )
17 13 cv 
 |-  h
18 17 ccnv 
 |-  `' h
19 cn 
 |-  NN
20 18 19 cima 
 |-  ( `' h " NN )
21 cfn 
 |-  Fin
22 20 21 wcel 
 |-  ( `' h " NN ) e. Fin
23 22 13 16 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
24 12 cv 
 |-  k
25 4 cv 
 |-  x
26 25 24 cfv 
 |-  ( k ` x )
27 caddc 
 |-  +
28 c1 
 |-  1
29 26 28 27 co 
 |-  ( ( k ` x ) + 1 )
30 cmg 
 |-  .g
31 9 30 cfv 
 |-  ( .g ` r )
32 6 cv 
 |-  f
33 27 cof 
 |-  oF +
34 vy 
 |-  y
35 34 cv 
 |-  y
36 35 25 wceq 
 |-  y = x
37 cc0 
 |-  0
38 36 28 37 cif 
 |-  if ( y = x , 1 , 0 )
39 34 5 38 cmpt 
 |-  ( y e. i |-> if ( y = x , 1 , 0 ) )
40 24 39 33 co 
 |-  ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) )
41 40 32 cfv 
 |-  ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) )
42 29 41 31 co 
 |-  ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) )
43 12 23 42 cmpt 
 |-  ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) )
44 6 11 43 cmpt 
 |-  ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) )
45 4 5 44 cmpt 
 |-  ( 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 oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) )
46 1 3 2 2 45 cmpo 
 |-  ( 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 oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )
47 0 46 wceq 
 |-  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 oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )