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{\upharpoonright }_{𝑠}{\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){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}=S{\upharpoonright }_{𝑠}{\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){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}r\right)}\right)$$
9		ovex	$$⊢S{\upharpoonright }_{𝑠}{\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{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
11		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
12		ress0	$$⊢\varnothing {\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}=\varnothing$$
13	11 12	eqtr4di	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing {\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
14		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{PwSer}}_1\left(R\right)=\varnothing$$
15	2 14	syl5eq	$$⊢\neg R\in \mathrm{V}\to S=\varnothing$$
16	15	oveq1d	$$⊢\neg R\in \mathrm{V}\to S{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}=\varnothing {\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17	13 16	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	10 17	pm2.61i	$$⊢{\mathrm{Poly}}_1\left(R\right)=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	1 18	eqtri	$$⊢P=S{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$