Definition df-ply1

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

	Ref	Expression
Assertion	df-ply1	⊢ Poly1 = ( 𝑟 ∈ V ↦ ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpl1	⊢ Poly1
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		cps1	⊢ PwSer1
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( PwSer1 ‘ 𝑟 )
6		cress	⊢ ↾s
7		cbs	⊢ Base
8		c1o	⊢ 1o
9		cmpl	⊢ mPoly
10	8 4 9	co	⊢ ( 1o mPoly 𝑟 )
11	10 7	cfv	⊢ ( Base ‘ ( 1o mPoly 𝑟 ) )
12	5 11 6	co	⊢ ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) )
13	1 2 12	cmpt	⊢ ( 𝑟 ∈ V ↦ ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) ) )
14	0 13	wceq	⊢ Poly1 = ( 𝑟 ∈ V ↦ ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) ) )