# Metamath Proof Explorer

## Theorem vr1cl

Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015)

Ref Expression
Hypotheses vr1cl.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
vr1cl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
vr1cl.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
Assertion vr1cl ${⊢}{R}\in \mathrm{Ring}\to {X}\in {B}$

### Proof

Step Hyp Ref Expression
1 vr1cl.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
2 vr1cl.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 vr1cl.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
4 1 vr1val ${⊢}{X}=\left({1}_{𝑜}\mathrm{mVar}{R}\right)\left(\varnothing \right)$
5 eqid ${⊢}{1}_{𝑜}\mathrm{mPoly}{R}={1}_{𝑜}\mathrm{mPoly}{R}$
6 eqid ${⊢}{1}_{𝑜}\mathrm{mVar}{R}={1}_{𝑜}\mathrm{mVar}{R}$
7 eqid ${⊢}{\mathrm{PwSer}}_{1}\left({R}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
8 2 7 3 ply1bas ${⊢}{B}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
9 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
10 9 a1i ${⊢}{R}\in \mathrm{Ring}\to {1}_{𝑜}\in \mathrm{\omega }$
11 id ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Ring}$
12 0lt1o ${⊢}\varnothing \in {1}_{𝑜}$
13 12 a1i ${⊢}{R}\in \mathrm{Ring}\to \varnothing \in {1}_{𝑜}$
14 5 6 8 10 11 13 mvrcl ${⊢}{R}\in \mathrm{Ring}\to \left({1}_{𝑜}\mathrm{mVar}{R}\right)\left(\varnothing \right)\in {B}$
15 4 14 eqeltrid ${⊢}{R}\in \mathrm{Ring}\to {X}\in {B}$