Definition df-ply1

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

	Ref	Expression
Assertion	df-ply1	|- Poly1 = ( r e. _V |-> ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpl1	|- Poly1
1		vr	|- r
2		cvv	|- _V
3		cps1	|- PwSer1
4	1	cv	|- r
5	4 3	cfv	|- ( PwSer1 ` r )
6		cress	|- |`s
7		cbs	|- Base
8		c1o	|- 1o
9		cmpl	|- mPoly
10	8 4 9	co	|- ( 1o mPoly r )
11	10 7	cfv	|- ( Base ` ( 1o mPoly r ) )
12	5 11 6	co	|- ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) )
13	1 2 12	cmpt	|- ( r e. _V |-> ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) ) )
14	0 13	wceq	|- Poly1 = ( r e. _V |-> ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) ) )