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

Definition df-mhp 16422
 Description: Define the subspaces of order- homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
df-mhp mHomP mPoly
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-mhp
StepHypRef Expression
1 cmhp 16411 . 2 mHomP
2 vi . . 3
3 vr . . 3
4 cvv 2956 . . 3
5 vn . . . 4
6 cn0 10221 . . . 4
7 vf . . . . . . . . 9
87cv 1651 . . . . . . . 8
98ccnv 4877 . . . . . . 7
103cv 1651 . . . . . . . . . 10
11 c0g 13723 . . . . . . . . . 10
1210, 11cfv 5454 . . . . . . . . 9
1312csn 3814 . . . . . . . 8
144, 13cdif 3317 . . . . . . 7
159, 14cima 4881 . . . . . 6
16 vj . . . . . . . . . . 11
1716cv 1651 . . . . . . . . . 10
18 vg . . . . . . . . . . 11
1918cv 1651 . . . . . . . . . 10
2017, 19cfv 5454 . . . . . . . . 9
216, 20, 16csu 12479 . . . . . . . 8
225cv 1651 . . . . . . . 8
2321, 22wceq 1652 . . . . . . 7
24 vh . . . . . . . . . . . 12
2524cv 1651 . . . . . . . . . . 11
2625ccnv 4877 . . . . . . . . . 10
27 cn 10000 . . . . . . . . . 10
2826, 27cima 4881 . . . . . . . . 9
29 cfn 7109 . . . . . . . . 9
3028, 29wcel 1725 . . . . . . . 8
312cv 1651 . . . . . . . . 9
32 cmap 7018 . . . . . . . . 9
336, 31, 32co 6081 . . . . . . . 8
3430, 24, 33crab 2709 . . . . . . 7
3523, 18, 34crab 2709 . . . . . 6
3615, 35wss 3320 . . . . 5
37 cmpl 16408 . . . . . . 7 mPoly
3831, 10, 37co 6081 . . . . . 6 mPoly
39 cbs 13469 . . . . . 6
4038, 39cfv 5454 . . . . 5 mPoly
4136, 7, 40crab 2709 . . . 4 mPoly
425, 6, 41cmpt 4266 . . 3 mPoly
432, 3, 4, 4, 42cmpt2 6083 . 2 mPoly
441, 43wceq 1652 1 mHomP mPoly
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator