# Metamath Proof Explorer

## Theorem ply1bas

Description: The value of the base set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses ply1val.1 ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
ply1val.2 ${⊢}{S}={\mathrm{PwSer}}_{1}\left({R}\right)$
ply1bas.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
Assertion ply1bas ${⊢}{U}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$

### Proof

Step Hyp Ref Expression
1 ply1val.1 ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ply1val.2 ${⊢}{S}={\mathrm{PwSer}}_{1}\left({R}\right)$
3 ply1bas.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
4 eqid ${⊢}{1}_{𝑜}\mathrm{mPoly}{R}={1}_{𝑜}\mathrm{mPoly}{R}$
5 eqid ${⊢}{1}_{𝑜}\mathrm{mPwSer}{R}={1}_{𝑜}\mathrm{mPwSer}{R}$
6 eqid ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
7 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
8 2 7 5 psr1bas2 ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPwSer}{R}\right)}$
9 4 5 6 8 mplbasss ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\subseteq {\mathrm{Base}}_{{S}}$
10 1 2 ply1val ${⊢}{P}={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
11 10 7 ressbas2 ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\subseteq {\mathrm{Base}}_{{S}}\to {\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}={\mathrm{Base}}_{{P}}$
12 9 11 ax-mp ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}={\mathrm{Base}}_{{P}}$
13 3 12 eqtr4i ${⊢}{U}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$