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

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

Detailed syntax breakdown of Definition df-mpl
StepHypRef Expression
1 cmpl 16089 . 2  class mPoly
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2788 . . 3  class  _V
5 vw . . . 4  set  w
62cv 1622 . . . . 5  class  i
73cv 1622 . . . . 5  class  r
8 cmps 16087 . . . . 5  class mPwSer
96, 7, 8co 5858 . . . 4  class  ( i mPwSer 
r )
105cv 1622 . . . . 5  class  w
11 vf . . . . . . . . . 10  set  f
1211cv 1622 . . . . . . . . 9  class  f
1312ccnv 4688 . . . . . . . 8  class  `' f
14 c0g 13400 . . . . . . . . . . 11  class  0g
157, 14cfv 5255 . . . . . . . . . 10  class  ( 0g
`  r )
1615csn 3640 . . . . . . . . 9  class  { ( 0g `  r ) }
174, 16cdif 3149 . . . . . . . 8  class  ( _V 
\  { ( 0g
`  r ) } )
1813, 17cima 4692 . . . . . . 7  class  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )
19 cfn 6863 . . . . . . 7  class  Fin
2018, 19wcel 1684 . . . . . 6  wff  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin
21 cbs 13148 . . . . . . 7  class  Base
2210, 21cfv 5255 . . . . . 6  class  ( Base `  w )
2320, 11, 22crab 2547 . . . . 5  class  { f  e.  ( Base `  w
)  |  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin }
24 cress 13149 . . . . 5  classs
2510, 23, 24co 5858 . . . 4  class  ( ws  { f  e.  ( Base `  w )  |  ( `' f " ( _V  \  { ( 0g
`  r ) } ) )  e.  Fin } )
265, 9, 25csb 3081 . . 3  class  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  ( `' f
" ( _V  \  { ( 0g `  r ) } ) )  e.  Fin }
)
272, 3, 4, 4, 26cmpt2 5860 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  ( `' f
" ( _V  \  { ( 0g `  r ) } ) )  e.  Fin }
) )
281, 27wceq 1623 1  wff mPoly  =  ( i  e.  _V , 
r  e.  _V  |->  [_ ( i mPwSer  r )  /  w ]_ ( ws  { f  e.  ( Base `  w )  |  ( `' f " ( _V  \  { ( 0g
`  r ) } ) )  e.  Fin } ) )
Colors of variables: wff set class
This definition is referenced by:  reldmmpl  16172  mplval  16173
  Copyright terms: Public domain W3C validator