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

Definition df-psd 16415
 Description: Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
df-psd mPSDer mPwSer .g
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-psd
StepHypRef Expression
1 cpsd 16404 . 2 mPSDer
2 vi . . 3
3 vr . . 3
4 cvv 2948 . . 3
5 vx . . . 4
62cv 1651 . . . 4
7 vf . . . . 5
83cv 1651 . . . . . . 7
9 cmps 16398 . . . . . . 7 mPwSer
106, 8, 9co 6073 . . . . . 6 mPwSer
11 cbs 13461 . . . . . 6
1210, 11cfv 5446 . . . . 5 mPwSer
13 vk . . . . . 6
14 vh . . . . . . . . . . 11
1514cv 1651 . . . . . . . . . 10
1615ccnv 4869 . . . . . . . . 9
17 cn 9992 . . . . . . . . 9
1816, 17cima 4873 . . . . . . . 8
19 cfn 7101 . . . . . . . 8
2018, 19wcel 1725 . . . . . . 7
21 cn0 10213 . . . . . . . 8
22 cmap 7010 . . . . . . . 8
2321, 6, 22co 6073 . . . . . . 7
2420, 14, 23crab 2701 . . . . . 6
255cv 1651 . . . . . . . . 9
2613cv 1651 . . . . . . . . 9
2725, 26cfv 5446 . . . . . . . 8
28 c1 8983 . . . . . . . 8
29 caddc 8985 . . . . . . . 8
3027, 28, 29co 6073 . . . . . . 7
31 vy . . . . . . . . . 10
3231, 5weq 1653 . . . . . . . . . . 11
33 cc0 8982 . . . . . . . . . . 11
3432, 28, 33cif 3731 . . . . . . . . . 10
3531, 6, 34cmpt 4258 . . . . . . . . 9
3629cof 6295 . . . . . . . . 9
3726, 35, 36co 6073 . . . . . . . 8
387cv 1651 . . . . . . . 8
3937, 38cfv 5446 . . . . . . 7
40 cmg 14681 . . . . . . . 8 .g
418, 40cfv 5446 . . . . . . 7 .g
4230, 39, 41co 6073 . . . . . 6 .g
4313, 24, 42cmpt 4258 . . . . 5 .g
447, 12, 43cmpt 4258 . . . 4 mPwSer .g
455, 6, 44cmpt 4258 . . 3 mPwSer .g
462, 3, 4, 4, 45cmpt2 6075 . 2 mPwSer .g
471, 46wceq 1652 1 mPSDer mPwSer .g
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator