df-ply1

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

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

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

Metamath Proof Explorer