MPE Home 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  =  ( 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 16408 . 2  class mPoly
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2956 . . 3  class  _V
5 vw . . . 4  set  w
62cv 1651 . . . . 5  class  i
73cv 1651 . . . . 5  class  r
8 cmps 16406 . . . . 5  class mPwSer
96, 7, 8co 6081 . . . 4  class  ( i mPwSer 
r )
105cv 1651 . . . . 5  class  w
11 vf . . . . . . . . . 10  set  f
1211cv 1651 . . . . . . . . 9  class  f
1312ccnv 4877 . . . . . . . 8  class  `' f
14 c0g 13723 . . . . . . . . . . 11  class  0g
157, 14cfv 5454 . . . . . . . . . 10  class  ( 0g
`  r )
1615csn 3814 . . . . . . . . 9  class  { ( 0g `  r ) }
174, 16cdif 3317 . . . . . . . 8  class  ( _V 
\  { ( 0g
`  r ) } )
1813, 17cima 4881 . . . . . . 7  class  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )
19 cfn 7109 . . . . . . 7  class  Fin
2018, 19wcel 1725 . . . . . 6  wff  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin
21 cbs 13469 . . . . . . 7  class  Base
2210, 21cfv 5454 . . . . . 6  class  ( Base `  w )
2320, 11, 22crab 2709 . . . . 5  class  { f  e.  ( Base `  w
)  |  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin }
24 cress 13470 . . . . 5  classs
2510, 23, 24co 6081 . . . 4  class  ( ws  { f  e.  ( Base `  w )  |  ( `' f " ( _V  \  { ( 0g
`  r ) } ) )  e.  Fin } )
265, 9, 25csb 3251 . . 3  class  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  ( `' f
" ( _V  \  { ( 0g `  r ) } ) )  e.  Fin }
)
272, 3, 4, 4, 26cmpt2 6083 . 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 1652 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  16491  mplval  16492
  Copyright terms: Public domain W3C validator