coe1fval2

Description: Univariate polynomial coefficient vectors expressed as a function composition. (Contributed by Stefan O'Rear, 21-Mar-2015)

Step	Hyp	Ref	Expression
1		coe1fval.a	$⊢ A = {coe}_{1} (F)$
2		coe1f.b	$⊢ B = {Base}_{P}$
3		coe1f.p	$⊢ P = {Poly}_{1} (R)$
4		coe1fval2.g	$⊢ G = (y \in ℕ_{0} ⟼ 1_{𝑜} \times \{y\})$
5	3 2	ply1bascl	$⊢ F \in B \to F \in {Base}_{{PwSer}_{1} (R)}$
6		eqid	$⊢ {Base}_{{PwSer}_{1} (R)} = {Base}_{{PwSer}_{1} (R)}$
7		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
8	1 6 7 4	coe1fval3	$⊢ F \in {Base}_{{PwSer}_{1} (R)} \to A = F \circ G$
9	5 8	syl	$⊢ F \in B \to A = F \circ G$

Metamath Proof Explorer