# Metamath Proof Explorer

## 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){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{r}\right)}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cpl1 ${class}{\mathrm{Poly}}_{1}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 cps1 ${class}{\mathrm{PwSer}}_{1}$
4 1 cv ${setvar}{r}$
5 4 3 cfv ${class}{\mathrm{PwSer}}_{1}\left({r}\right)$
6 cress ${class}{↾}_{𝑠}$
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){↾}_{𝑠}{\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){↾}_{𝑠}{\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){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{r}\right)}\right)$