Metamath Proof Explorer


Definition df-mpl

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)

Ref Expression
Assertion df-mpl
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpl
 |-  mPoly
1 vi
 |-  i
2 cvv
 |-  _V
3 vr
 |-  r
4 1 cv
 |-  i
5 cmps
 |-  mPwSer
6 3 cv
 |-  r
7 4 6 5 co
 |-  ( i mPwSer r )
8 vw
 |-  w
9 8 cv
 |-  w
10 cress
 |-  |`s
11 vf
 |-  f
12 cbs
 |-  Base
13 9 12 cfv
 |-  ( Base ` w )
14 11 cv
 |-  f
15 cfsupp
 |-  finSupp
16 c0g
 |-  0g
17 6 16 cfv
 |-  ( 0g ` r )
18 14 17 15 wbr
 |-  f finSupp ( 0g ` r )
19 18 11 13 crab
 |-  { f e. ( Base ` w ) | f finSupp ( 0g ` r ) }
20 9 19 10 co
 |-  ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
21 8 7 20 csb
 |-  [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
22 1 3 2 2 21 cmpo
 |-  ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )
23 0 22 wceq
 |-  mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )