Theorem psr1bascl

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

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

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
2		psr1rcl.b	$$⊢B={\mathrm{Base}}_P$$
3		id	$$⊢F\in B\to F\in B$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
5	1 2 4	psr1bas2	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
6	3 5	eleqtrdi	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$