Definition df-ply1

Description: Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Assertion	df-ply1	$$⊢{\mathrm{Poly}}_1=\left(r\in \mathrm{V}⟼{\mathrm{PwSer}}_1\left(r\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpl1	$$class{\mathrm{Poly}}_1$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		cps1	$$class{\mathrm{PwSer}}_1$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{\mathrm{PwSer}}_1\left(r\right)$$
6		cress	$$class{\upharpoonright }_{𝑠}$$
7		cbs	$$class\mathrm{Base}$$
8		c1o	$$class{1}_{𝑜}$$
9		cmpl	$$class\mathrm{mPoly}$$
10	8 4 9	co	$$class\left(1_{𝑜}\mathrm{mPoly}r\right)$$
11	10 7	cfv	$$class{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}$$
12	5 11 6	co	$$class\left({\mathrm{PwSer}}_1\left(r\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}\right)$$
13	1 2 12	cmpt	$$class\left(r\in \mathrm{V}⟼{\mathrm{PwSer}}_1\left(r\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}\right)$$
14	0 13	wceq	$$wff{\mathrm{Poly}}_1=\left(r\in \mathrm{V}⟼{\mathrm{PwSer}}_1\left(r\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}\right)$$