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 = ( coe1 ` F )
	coe1f.b	|- B = ( Base ` P )
	coe1f.p	|- P = ( Poly1 ` R )
	coe1fval2.g	|- G = ( y e. NN0 |-> ( 1o X. { y } ) )
Assertion	coe1fval2	|- ( F e. B -> A = ( F o. G ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	|- A = ( coe1 ` F )
2		coe1f.b	|- B = ( Base ` P )
3		coe1f.p	|- P = ( Poly1 ` R )
4		coe1fval2.g	|- G = ( y e. NN0 |-> ( 1o X. { y } ) )
5	3 2	ply1bascl	|- ( F e. B -> F e. ( Base ` ( PwSer1 ` R ) ) )
6		eqid	|- ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
7		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
8	1 6 7 4	coe1fval3	|- ( F e. ( Base ` ( PwSer1 ` R ) ) -> A = ( F o. G ) )
9	5 8	syl	|- ( F e. B -> A = ( F o. G ) )