Definition df-coe1

Description: Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Assertion	df-coe1	|- coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cco1	|- coe1
1		vf	|- f
2		cvv	|- _V
3		vn	|- n
4		cn0	|- NN0
5	1	cv	|- f
6		c1o	|- 1o
7	3	cv	|- n
8	7	csn	|- { n }
9	6 8	cxp	|- ( 1o X. { n } )
10	9 5	cfv	|- ( f ` ( 1o X. { n } ) )
11	3 4 10	cmpt	|- ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) )
12	1 2 11	cmpt	|- ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )
13	0 12	wceq	|- coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )