Theorem coe1f

Description: Functionality of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
	coe1f.b	$$⊢B={\mathrm{Base}}_P$$
	coe1f.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1f.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	coe1f	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		coe1f.b	$$⊢B={\mathrm{Base}}_P$$
3		coe1f.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		coe1f.k	$$⊢K={\mathrm{Base}}_R$$
5	3 2	ply1bascl	$$⊢F\in B\to F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
6		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
7		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
8	1 6 7 4	coe1f2	$$⊢F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\to A:{\mathbb{N}}_0⟶K$$
9	5 8	syl	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$