Definition df-mpl 17806

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

Assertion

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

Distinct variable group:   f, i, r, w

Detailed syntax breakdown of Definition df-mpl

Step	Hyp	Ref	Expression
1		cmpl 17801	. 2 class mPoly
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3113	. . 3 class _V
5		vw	. . . 4 setvar w
6	2	cv 1378	. . . . 5 class i
7	3	cv 1378	. . . . 5 class r
8		cmps 17799	. . . . 5 class mPwSer
9	6, 7, 8	co 6284	. . . 4 class ( i mPwSer r )
10	5	cv 1378	. . . . 5 class w
11		vf	. . . . . . . 8 setvar f
12	11	cv 1378	. . . . . . 7 class f
13		c0g 14695	. . . . . . . 8 class 0g
14	7, 13	cfv 5588	. . . . . . 7 class ( 0g ` r )
15		cfsupp 7829	. . . . . . 7 class finSupp
16	12, 14, 15	wbr 4447	. . . . . 6 wff f finSupp ( 0g ` r )
17		cbs 14490	. . . . . . 7 class Base
18	10, 17	cfv 5588	. . . . . 6 class ( Base ` w )
19	16, 11, 18	crab 2818	. . . . 5 class { f e. ( Base ` w ) | f finSupp ( 0g ` r ) }
20		cress 14491	. . . . 5 class ↾s
21	10, 19, 20	co 6284	. . . 4 class ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
22	5, 9, 21	csb 3435	. . 3 class [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
23	2, 3, 4, 4, 22	cmpt2 6286	. 2 class ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )
24	1, 23	wceq 1379	1 wff mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) )

This definition is referenced by:  reldmmpl  17882  mplval  17883