Theorem coe1f

Description: Functionality of univariate polynomial coefficient vectors. (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 )
	coe1f.k	|- K = ( Base ` R )
Assertion	coe1f	|- ( F e. B -> A : NN0 --> K )

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	|- A = ( coe1 ` F )
2		coe1f.b	|- B = ( Base ` P )
3		coe1f.p	|- P = ( Poly1 ` R )
4		coe1f.k	|- K = ( Base ` R )
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	coe1f2	|- ( F e. ( Base ` ( PwSer1 ` R ) ) -> A : NN0 --> K )
9	5 8	syl	|- ( F e. B -> A : NN0 --> K )