Definition df-mplcoe 14799

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.) (Revised by Jim Kingdon, 7-Oct-2025.)

Assertion

Ref	Expression
df-mplcoe	|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )

Distinct variable group:   a, b, f, i, k, r, w

Detailed syntax breakdown of Definition df-mplcoe

Step	Hyp	Ref	Expression
1		cmpl 14797	. 2 class mPoly
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 2812	. . 3 class _V
5		vw	. . . 4 setvar w
6	2	cv 1397	. . . . 5 class i
7	3	cv 1397	. . . . 5 class r
8		cmps 14796	. . . . 5 class mPwSer
9	6, 7, 8	co 6049	. . . 4 class ( i mPwSer r )
10	5	cv 1397	. . . . 5 class w
11		vk	. . . . . . . . . . . . 13 setvar k
12	11	cv 1397	. . . . . . . . . . . 12 class k
13		va	. . . . . . . . . . . . 13 setvar a
14	13	cv 1397	. . . . . . . . . . . 12 class a
15	12, 14	cfv 5351	. . . . . . . . . . 11 class ( a ` k )
16		vb	. . . . . . . . . . . . 13 setvar b
17	16	cv 1397	. . . . . . . . . . . 12 class b
18	12, 17	cfv 5351	. . . . . . . . . . 11 class ( b ` k )
19		clt 8304	. . . . . . . . . . 11 class <
20	15, 18, 19	wbr 4108	. . . . . . . . . 10 wff ( a ` k ) < ( b ` k )
21	20, 11, 6	wral 2520	. . . . . . . . 9 wff A. k e. i ( a ` k ) < ( b ` k )
22		vf	. . . . . . . . . . . 12 setvar f
23	22	cv 1397	. . . . . . . . . . 11 class f
24	17, 23	cfv 5351	. . . . . . . . . 10 class ( f ` b )
25		c0g 13458	. . . . . . . . . . 11 class 0g
26	7, 25	cfv 5351	. . . . . . . . . 10 class ( 0g ` r )
27	24, 26	wceq 1398	. . . . . . . . 9 wff ( f ` b ) = ( 0g ` r )
28	21, 27	wi 4	. . . . . . . 8 wff ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) )
29		cn0 9492	. . . . . . . . 9 class NN0
30		cmap 6881	. . . . . . . . 9 class ^m
31	29, 6, 30	co 6049	. . . . . . . 8 class ( NN0 ^m i )
32	28, 16, 31	wral 2520	. . . . . . 7 wff A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) )
33	32, 13, 31	wrex 2521	. . . . . 6 wff E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) )
34		cbs 13201	. . . . . . 7 class Base
35	10, 34	cfv 5351	. . . . . 6 class ( Base ` w )
36	33, 22, 35	crab 2524	. . . . 5 class { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) }
37		cress 13202	. . . . 5 class ↾s
38	10, 36, 37	co 6049	. . . 4 class ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } )
39	5, 9, 38	csb 3137	. . 3 class [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } )
40	2, 3, 4, 4, 39	cmpo 6051	. 2 class ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
41	1, 40	wceq 1398	1 wff mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )

This definition is referenced by:  reldmmpl  14831  mplvalcoe  14832  fnmpl  14835