# Metamath Proof Explorer

## Theorem ply1val

Description: The value of the 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)$
Assertion ply1val ${⊢}{P}={S}{↾}_{𝑠}{\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 fveq2 ${⊢}{r}={R}\to {\mathrm{PwSer}}_{1}\left({r}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
4 3 2 eqtr4di ${⊢}{r}={R}\to {\mathrm{PwSer}}_{1}\left({r}\right)={S}$
5 oveq2 ${⊢}{r}={R}\to {1}_{𝑜}\mathrm{mPoly}{r}={1}_{𝑜}\mathrm{mPoly}{R}$
6 5 fveq2d ${⊢}{r}={R}\to {\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{r}\right)}={\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
7 4 6 oveq12d ${⊢}{r}={R}\to {\mathrm{PwSer}}_{1}\left({r}\right){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{r}\right)}={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
8 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)$
9 ovex ${⊢}{S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{V}$
10 7 8 9 fvmpt ${⊢}{R}\in \mathrm{V}\to {\mathrm{Poly}}_{1}\left({R}\right)={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
11 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{Poly}}_{1}\left({R}\right)=\varnothing$
12 ress0 ${⊢}\varnothing {↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}=\varnothing$
13 11 12 eqtr4di ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{Poly}}_{1}\left({R}\right)=\varnothing {↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
14 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{PwSer}}_{1}\left({R}\right)=\varnothing$
15 2 14 syl5eq ${⊢}¬{R}\in \mathrm{V}\to {S}=\varnothing$
16 15 oveq1d ${⊢}¬{R}\in \mathrm{V}\to {S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}=\varnothing {↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
17 13 16 eqtr4d ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{Poly}}_{1}\left({R}\right)={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
18 10 17 pm2.61i ${⊢}{\mathrm{Poly}}_{1}\left({R}\right)={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
19 1 18 eqtri ${⊢}{P}={S}{↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$