Definition df-coe1 17538

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

Assertion

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

Distinct variable group:   f, n

Detailed syntax breakdown of Definition df-coe1

Step	Hyp	Ref	Expression
1		cco1 17531	. 2 class coe1
2		vf	. . 3 setvar f
3		cvv 2962	. . 3 class _V
4		vn	. . . 4 setvar n
5		cn0 10567	. . . 4 class NN0
6		c1o 6901	. . . . . 6 class 1o
7	4	cv 1361	. . . . . . 7 class n
8	7	csn 3865	. . . . . 6 class { n }
9	6, 8	cxp 4825	. . . . 5 class ( 1o X. { n } )
10	2	cv 1361	. . . . 5 class f
11	9, 10	cfv 5406	. . . 4 class ( f ` ( 1o X. { n } ) )
12	4, 5, 11	cmpt 4338	. . 3 class ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) )
13	2, 3, 12	cmpt 4338	. 2 class ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )
14	1, 13	wceq 1362	1 wff coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )

This definition is referenced by:  coe1fval  17560