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

Definition df-mpl 18582
 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.) (Revised by AV, 25-Jun-2019.)
Assertion
Ref Expression
df-mpl mPoly mPwSer s finSupp
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-mpl
StepHypRef Expression
1 cmpl 18577 . 2 mPoly
2 vi . . 3
3 vr . . 3
4 cvv 3045 . . 3
5 vw . . . 4
62cv 1443 . . . . 5
73cv 1443 . . . . 5
8 cmps 18575 . . . . 5 mPwSer
96, 7, 8co 6290 . . . 4 mPwSer
105cv 1443 . . . . 5
11 vf . . . . . . . 8
1211cv 1443 . . . . . . 7
13 c0g 15338 . . . . . . . 8
147, 13cfv 5582 . . . . . . 7
15 cfsupp 7883 . . . . . . 7 finSupp
1612, 14, 15wbr 4402 . . . . . 6 finSupp
17 cbs 15121 . . . . . . 7
1810, 17cfv 5582 . . . . . 6
1916, 11, 18crab 2741 . . . . 5 finSupp
20 cress 15122 . . . . 5 s
2110, 19, 20co 6290 . . . 4 s finSupp
225, 9, 21csb 3363 . . 3 mPwSer s finSupp
232, 3, 4, 4, 22cmpt2 6292 . 2 mPwSer s finSupp
241, 23wceq 1444 1 mPoly mPwSer s finSupp
 Colors of variables: wff setvar class This definition is referenced by:  reldmmpl  18651  mplval  18652
 Copyright terms: Public domain W3C validator