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

Definition df-mpl 18202
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  =  ( i  e.  _V , 
r  e.  _V  |->  [_ ( i mPwSer  r )  /  w ]_ ( ws  { f  e.  ( Base `  w )  |  f finSupp 
( 0g `  r
) } ) )
Distinct variable group:    f, i, r, w

Detailed syntax breakdown of Definition df-mpl
StepHypRef Expression
1 cmpl 18197 . 2  class mPoly
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 3106 . . 3  class  _V
5 vw . . . 4  setvar  w
62cv 1397 . . . . 5  class  i
73cv 1397 . . . . 5  class  r
8 cmps 18195 . . . . 5  class mPwSer
96, 7, 8co 6270 . . . 4  class  ( i mPwSer 
r )
105cv 1397 . . . . 5  class  w
11 vf . . . . . . . 8  setvar  f
1211cv 1397 . . . . . . 7  class  f
13 c0g 14929 . . . . . . . 8  class  0g
147, 13cfv 5570 . . . . . . 7  class  ( 0g
`  r )
15 cfsupp 7821 . . . . . . 7  class finSupp
1612, 14, 15wbr 4439 . . . . . 6  wff  f finSupp  ( 0g `  r )
17 cbs 14716 . . . . . . 7  class  Base
1810, 17cfv 5570 . . . . . 6  class  ( Base `  w )
1916, 11, 18crab 2808 . . . . 5  class  { f  e.  ( Base `  w
)  |  f finSupp  ( 0g `  r ) }
20 cress 14717 . . . . 5  classs
2110, 19, 20co 6270 . . . 4  class  ( ws  { f  e.  ( Base `  w )  |  f finSupp 
( 0g `  r
) } )
225, 9, 21csb 3420 . . 3  class  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  f finSupp  ( 0g `  r ) } )
232, 3, 4, 4, 22cmpt2 6272 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  f finSupp  ( 0g `  r ) } ) )
241, 23wceq 1398 1  wff mPoly  =  ( i  e.  _V , 
r  e.  _V  |->  [_ ( i mPwSer  r )  /  w ]_ ( ws  { f  e.  ( Base `  w )  |  f finSupp 
( 0g `  r
) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  reldmmpl  18278  mplval  18279
  Copyright terms: Public domain W3C validator