# Metamath Proof Explorer

## Theorem ply1ring

Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypothesis ply1ring.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
Assertion ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 ply1ring.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 eqid ${⊢}{\mathrm{PwSer}}_{1}\left({R}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
4 1 2 3 ply1bas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
5 1 2 3 ply1subrg ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{Base}}_{{P}}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_{1}\left({R}\right)\right)$
6 4 5 eqeltrrid ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_{1}\left({R}\right)\right)$
7 1 2 ply1val ${⊢}{P}={\mathrm{PwSer}}_{1}\left({R}\right){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
8 7 subrgring ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_{1}\left({R}\right)\right)\to {P}\in \mathrm{Ring}$
9 6 8 syl ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$