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 ) } ) )