Definition df-mplcoe 14681

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 14679	. 2 class mPoly
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 2802	. . 3 class _V
5		vw	. . . 4 setvar w
6	2	cv 1396	. . . . 5 class i
7	3	cv 1396	. . . . 5 class r
8		cmps 14678	. . . . 5 class mPwSer
9	6, 7, 8	co 6018	. . . 4 class ( i mPwSer r )
10	5	cv 1396	. . . . 5 class w
11		vk	. . . . . . . . . . . . 13 setvar k
12	11	cv 1396	. . . . . . . . . . . 12 class k
13		va	. . . . . . . . . . . . 13 setvar a
14	13	cv 1396	. . . . . . . . . . . 12 class a
15	12, 14	cfv 5326	. . . . . . . . . . 11 class ( a ` k )
16		vb	. . . . . . . . . . . . 13 setvar b
17	16	cv 1396	. . . . . . . . . . . 12 class b
18	12, 17	cfv 5326	. . . . . . . . . . 11 class ( b ` k )
19		clt 8214	. . . . . . . . . . 11 class <
20	15, 18, 19	wbr 4088	. . . . . . . . . 10 wff ( a ` k ) < ( b ` k )
21	20, 11, 6	wral 2510	. . . . . . . . 9 wff A. k e. i ( a ` k ) < ( b ` k )
22		vf	. . . . . . . . . . . 12 setvar f
23	22	cv 1396	. . . . . . . . . . 11 class f
24	17, 23	cfv 5326	. . . . . . . . . 10 class ( f ` b )
25		c0g 13341	. . . . . . . . . . 11 class 0g
26	7, 25	cfv 5326	. . . . . . . . . 10 class ( 0g ` r )
27	24, 26	wceq 1397	. . . . . . . . 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 9402	. . . . . . . . 9 class NN0
30		cmap 6817	. . . . . . . . 9 class ^m
31	29, 6, 30	co 6018	. . . . . . . 8 class ( NN0 ^m i )
32	28, 16, 31	wral 2510	. . . . . . 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 2511	. . . . . 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 13084	. . . . . . 7 class Base
35	10, 34	cfv 5326	. . . . . 6 class ( Base ` w )
36	33, 22, 35	crab 2514	. . . . 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 13085	. . . . 5 class ↾s
38	10, 36, 37	co 6018	. . . 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 3127	. . 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 6020	. 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 1397	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  14706  mplvalcoe  14707  fnmpl  14710