Definition df-mpl 16374

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

Assertion

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

Distinct variable group:   f, i, r, w

Detailed syntax breakdown of Definition df-mpl

Step	Hyp	Ref	Expression
1		cmpl 16363	. 2 class mPoly
2		vi	. . 3 set i
3		vr	. . 3 set r
4		cvv 2916	. . 3 class _V
5		vw	. . . 4 set w
6	2	cv 1648	. . . . 5 class i
7	3	cv 1648	. . . . 5 class r
8		cmps 16361	. . . . 5 class mPwSer
9	6, 7, 8	co 6040	. . . 4 class ( i mPwSer r )
10	5	cv 1648	. . . . 5 class w
11		vf	. . . . . . . . . 10 set f
12	11	cv 1648	. . . . . . . . 9 class f
13	12	ccnv 4836	. . . . . . . 8 class `' f
14		c0g 13678	. . . . . . . . . . 11 class 0g
15	7, 14	cfv 5413	. . . . . . . . . 10 class ( 0g ` r )
16	15	csn 3774	. . . . . . . . 9 class { ( 0g ` r ) }
17	4, 16	cdif 3277	. . . . . . . 8 class ( _V \ { ( 0g ` r ) } )
18	13, 17	cima 4840	. . . . . . 7 class ( `' f " ( _V \ { ( 0g ` r ) } ) )
19		cfn 7068	. . . . . . 7 class Fin
20	18, 19	wcel 1721	. . . . . 6 wff ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin
21		cbs 13424	. . . . . . 7 class Base
22	10, 21	cfv 5413	. . . . . 6 class ( Base ` w )
23	20, 11, 22	crab 2670	. . . . 5 class { f e. ( Base ` w ) | ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin }
24		cress 13425	. . . . 5 class ↾s
25	10, 23, 24	co 6040	. . . 4 class ( w ↾s { f e. ( Base ` w ) | ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin } )
26	5, 9, 25	csb 3211	. . 3 class [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin } )
27	2, 3, 4, 4, 26	cmpt2 6042	. 2 class ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin } ) )
28	1, 27	wceq 1649	1 wff mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | ( `' f " ( _V \ { ( 0g ` r ) } ) ) e. Fin } ) )

This definition is referenced by:  reldmmpl  16446  mplval  16447