Theorem ply1bascl2

Description: A univariate polynomial is a multivariate polynomial on one index. (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	ply1bascl2	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}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 2	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
5	4	eleq2i	$$⊢F\in B\leftrightarrow F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
6	5	biimpi	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$