Theorem coe1fval2

Description: Univariate polynomial coefficient vectors expressed as a function composition. (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)$$
	coe1fval2.g	$$⊢G=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
Assertion	coe1fval2	$$⊢F\in B\to A=F\circ G$$

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		coe1fval2.g	$$⊢G=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
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	coe1fval3	$$⊢F\in {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\to A=F\circ G$$
9	5 8	syl	$$⊢F\in B\to A=F\circ G$$