Definition df-coe1 16536

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 16529	. 2 class coe1
2		vf	. . 3 set f
3		cvv 2916	. . 3 class _V
4		vn	. . . 4 set n
5		cn0 10177	. . . 4 class NN0
6		c1o 6676	. . . . . 6 class 1o
7	4	cv 1648	. . . . . . 7 class n
8	7	csn 3774	. . . . . 6 class { n }
9	6, 8	cxp 4835	. . . . 5 class ( 1o X. { n } )
10	2	cv 1648	. . . . 5 class f
11	9, 10	cfv 5413	. . . 4 class ( f ` ( 1o X. { n } ) )
12	4, 5, 11	cmpt 4226	. . 3 class ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) )
13	2, 3, 12	cmpt 4226	. 2 class ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )
14	1, 13	wceq 1649	1 wff coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )

This definition is referenced by:  coe1fval  16558