Definition df-mpl 15158

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

The index set (which has an element for each variable) is i, the coefficients are in ring r, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for r). (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 15155	. 2 class mPoly
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 2821	. . 3 class _V
5		vw	. . . 4 setvar w
6	2	cv 1401	. . . . 5 class i
7	3	cv 1401	. . . . 5 class r
8		cmps 15153	. . . . 5 class mPwSer
9	6, 7, 8	co 6088	. . . 4 class ( i mPwSer r )
10	5	cv 1401	. . . . 5 class w
11		vf	. . . . . . . 8 setvar f
12	11	cv 1401	. . . . . . 7 class f
13		c0g 13668	. . . . . . . 8 class 0g
14	7, 13	cfv 5380	. . . . . . 7 class ( 0g ` r )
15		cfsupp 7292	. . . . . . 7 class finSupp
16	12, 14, 15	wbr 4131	. . . . . 6 wff f finSupp ( 0g ` r )
17		cbs 13409	. . . . . . 7 class Base
18	10, 17	cfv 5380	. . . . . 6 class ( Base ` w )
19	16, 11, 18	crab 2532	. . . . 5 class { f e. ( Base ` w ) | f finSupp ( 0g ` r ) }
20		cress 13410	. . . . 5 class ↾s
21	10, 19, 20	co 6088	. . . 4 class ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
22	5, 9, 21	csb 3147	. . 3 class [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
23	2, 3, 4, 4, 22	cmpo 6090	. 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 1402	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 used by:  reldmmpl  15221  mplvalg  15222  mplbas  15223  fnmpl  15225