Theorem ply1bascl

Description: A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	ply1bascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1bascl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	ply1bascl	$$⊢F\in B\to F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$

Proof

Step	Hyp	Ref	Expression
1		ply1bascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1bascl.b	$$⊢B={\mathrm{Base}}_P$$
3		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
4	1 3	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
5		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
6	4 5	ressbasss	$$⊢{\mathrm{Base}}_P\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
7	2 6	eqsstri	$$⊢B\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
8	7	sseli	$$⊢F\in B\to F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$