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

Definition df-mpl 16419
 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 16408 . 2 mPoly
2 vi . . 3
3 vr . . 3
4 cvv 2956 . . 3
5 vw . . . 4
62cv 1651 . . . . 5
73cv 1651 . . . . 5
8 cmps 16406 . . . . 5 mPwSer
96, 7, 8co 6081 . . . 4 mPwSer
105cv 1651 . . . . 5
11 vf . . . . . . . . . 10
1211cv 1651 . . . . . . . . 9
1312ccnv 4877 . . . . . . . 8
14 c0g 13723 . . . . . . . . . . 11
157, 14cfv 5454 . . . . . . . . . 10
1615csn 3814 . . . . . . . . 9
174, 16cdif 3317 . . . . . . . 8
1813, 17cima 4881 . . . . . . 7
19 cfn 7109 . . . . . . 7
2018, 19wcel 1725 . . . . . 6
21 cbs 13469 . . . . . . 7
2210, 21cfv 5454 . . . . . 6
2320, 11, 22crab 2709 . . . . 5
24 cress 13470 . . . . 5 s
2510, 23, 24co 6081 . . . 4 s
265, 9, 25csb 3251 . . 3 mPwSer s
272, 3, 4, 4, 26cmpt2 6083 . 2 mPwSer s
281, 27wceq 1652 1 mPoly mPwSer s
 Colors of variables: wff set class This definition is referenced by:  reldmmpl  16491  mplval  16492
 Copyright terms: Public domain W3C validator