Definition df-mpl 17875

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 17870	. 2 class mPoly
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3093	. . 3 class _V
5		vw	. . . 4 setvar w
6	2	cv 1380	. . . . 5 class i
7	3	cv 1380	. . . . 5 class r
8		cmps 17868	. . . . 5 class mPwSer
9	6, 7, 8	co 6277	. . . 4 class ( i mPwSer r )
10	5	cv 1380	. . . . 5 class w
11		vf	. . . . . . . 8 setvar f
12	11	cv 1380	. . . . . . 7 class f
13		c0g 14709	. . . . . . . 8 class 0g
14	7, 13	cfv 5574	. . . . . . 7 class ( 0g ` r )
15		cfsupp 7827	. . . . . . 7 class finSupp
16	12, 14, 15	wbr 4433	. . . . . 6 wff f finSupp ( 0g ` r )
17		cbs 14504	. . . . . . 7 class Base
18	10, 17	cfv 5574	. . . . . 6 class ( Base ` w )
19	16, 11, 18	crab 2795	. . . . 5 class { f e. ( Base ` w ) | f finSupp ( 0g ` r ) }
20		cress 14505	. . . . 5 class ↾s
21	10, 19, 20	co 6277	. . . 4 class ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
22	5, 9, 21	csb 3417	. . 3 class [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } )
23	2, 3, 4, 4, 22	cmpt2 6279	. 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 1381	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  17951  mplval  17952