Theorem ply1sca

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypothesis	ply1lmod.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1sca	$$⊢R\in V\to R=\mathrm{Scalar}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1lmod.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
3	2	psr1sca	$$⊢R\in V\to R=\mathrm{Scalar}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
4		fvex	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{V}$$
5	1 2	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
6		eqid	$$⊢\mathrm{Scalar}\left({\mathrm{PwSer}}_1\left(R\right)\right)=\mathrm{Scalar}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
7	5 6	resssca	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{V}\to \mathrm{Scalar}\left({\mathrm{PwSer}}_1\left(R\right)\right)=\mathrm{Scalar}\left(P\right)$$
8	4 7	ax-mp	$$⊢\mathrm{Scalar}\left({\mathrm{PwSer}}_1\left(R\right)\right)=\mathrm{Scalar}\left(P\right)$$
9	3 8	eqtrdi	$$⊢R\in V\to R=\mathrm{Scalar}\left(P\right)$$