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

Definition df-mpl 16374
 Description: Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
df-mpl mPoly mPwSer s
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-mpl
StepHypRef Expression
1 cmpl 16363 . 2 mPoly
2 vi . . 3
3 vr . . 3
4 cvv 2916 . . 3
5 vw . . . 4
62cv 1648 . . . . 5
73cv 1648 . . . . 5
8 cmps 16361 . . . . 5 mPwSer
96, 7, 8co 6040 . . . 4 mPwSer
105cv 1648 . . . . 5
11 vf . . . . . . . . . 10
1211cv 1648 . . . . . . . . 9
1312ccnv 4836 . . . . . . . 8
14 c0g 13678 . . . . . . . . . . 11
157, 14cfv 5413 . . . . . . . . . 10
1615csn 3774 . . . . . . . . 9
174, 16cdif 3277 . . . . . . . 8
1813, 17cima 4840 . . . . . . 7
19 cfn 7068 . . . . . . 7
2018, 19wcel 1721 . . . . . 6
21 cbs 13424 . . . . . . 7
2210, 21cfv 5413 . . . . . 6
2320, 11, 22crab 2670 . . . . 5
24 cress 13425 . . . . 5 s
2510, 23, 24co 6040 . . . 4 s
265, 9, 25csb 3211 . . 3 mPwSer s
272, 3, 4, 4, 26cmpt2 6042 . 2 mPwSer s
281, 27wceq 1649 1 mPoly mPwSer s
 Colors of variables: wff set class This definition is referenced by:  reldmmpl  16446  mplval  16447
 Copyright terms: Public domain W3C validator