Theorem ply1basf

Description: Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	ply1rcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1rcl.b	$$⊢B={\mathrm{Base}}_P$$
	ply1basf.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	ply1basf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$

Proof

Step	Hyp	Ref	Expression
1		ply1rcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1rcl.b	$$⊢B={\mathrm{Base}}_P$$
3		ply1basf.k	$$⊢K={\mathrm{Base}}_R$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
5		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
6		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{a\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		id	$$⊢F\in B\to F\in B$$
8		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
9	1 8 2	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
10	7 9	eleqtrdi	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
11	4 3 5 6 10	mplelf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$