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

Definition df-mpl 16116
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 16105 . 2  class mPoly
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vw . . . 4  set  w
62cv 1631 . . . . 5  class  i
73cv 1631 . . . . 5  class  r
8 cmps 16103 . . . . 5  class mPwSer
96, 7, 8co 5874 . . . 4  class  ( i mPwSer 
r )
105cv 1631 . . . . 5  class  w
11 vf . . . . . . . . . 10  set  f
1211cv 1631 . . . . . . . . 9  class  f
1312ccnv 4704 . . . . . . . 8  class  `' f
14 c0g 13416 . . . . . . . . . . 11  class  0g
157, 14cfv 5271 . . . . . . . . . 10  class  ( 0g
`  r )
1615csn 3653 . . . . . . . . 9  class  { ( 0g `  r ) }
174, 16cdif 3162 . . . . . . . 8  class  ( _V 
\  { ( 0g
`  r ) } )
1813, 17cima 4708 . . . . . . 7  class  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )
19 cfn 6879 . . . . . . 7  class  Fin
2018, 19wcel 1696 . . . . . 6  wff  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin
21 cbs 13164 . . . . . . 7  class  Base
2210, 21cfv 5271 . . . . . 6  class  ( Base `  w )
2320, 11, 22crab 2560 . . . . 5  class  { f  e.  ( Base `  w
)  |  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  e.  Fin }
24 cress 13165 . . . . 5  classs
2510, 23, 24co 5874 . . . 4  class  ( ws  { f  e.  ( Base `  w )  |  ( `' f " ( _V  \  { ( 0g
`  r ) } ) )  e.  Fin } )
265, 9, 25csb 3094 . . 3  class  [_ (
i mPwSer  r )  /  w ]_ ( ws  { f  e.  (
Base `  w )  |  ( `' f
" ( _V  \  { ( 0g `  r ) } ) )  e.  Fin }
)
272, 3, 4, 4, 26cmpt2 5876 . 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 1632 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  16188  mplval  16189
  Copyright terms: Public domain W3C validator