Definition df-mpl

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)

	Ref	Expression
Assertion	df-mpl	$$⊢\mathrm{mPoly}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left(i\mathrm{mPwSer}r\right)/w⦌\left(w{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpl	$$class\mathrm{mPoly}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4	1	cv	$$setvari$$
5		cmps	$$class\mathrm{mPwSer}$$
6	3	cv	$$setvarr$$
7	4 6 5	co	$$class\left(i\mathrm{mPwSer}r\right)$$
8		vw	$$setvarw$$
9	8	cv	$$setvarw$$
10		cress	$$class{\upharpoonright }_{𝑠}$$
11		vf	$$setvarf$$
12		cbs	$$class\mathrm{Base}$$
13	9 12	cfv	$$class{\mathrm{Base}}_w$$
14	11	cv	$$setvarf$$
15		cfsupp	$$class\mathrm{finSupp}$$
16		c0g	$$class{0}_{𝑔}$$
17	6 16	cfv	$$class{0}_r$$
18	14 17 15	wbr	$$wff{finSupp}_{0_r}\left(f\right)$$
19	18 11 13	crab	$$class\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}$$
20	9 19 10	co	$$class\left(w{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}\right)$$
21	8 7 20	csb	$$class⦋\left(i\mathrm{mPwSer}r\right)/w⦌\left(w{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}\right)$$
22	1 3 2 2 21	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left(i\mathrm{mPwSer}r\right)/w⦌\left(w{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}\right)\right)$$
23	0 22	wceq	$$wff\mathrm{mPoly}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left(i\mathrm{mPwSer}r\right)/w⦌\left(w{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_w|{finSupp}_{0_r}\left(f\right)\right\}\right)\right)$$