Definition df-coe1 19553

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 19548	. 2 class coe1
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4		vn	. . . 4 setvar n
5		cn0 11292	. . . 4 class NN0
6		c1o 7553	. . . . . 6 class 1o
7	4	cv 1482	. . . . . . 7 class n
8	7	csn 4177	. . . . . 6 class { n }
9	6, 8	cxp 5112	. . . . 5 class ( 1o X. { n } )
10	2	cv 1482	. . . . 5 class f
11	9, 10	cfv 5888	. . . 4 class ( f ` ( 1o X. { n } ) )
12	4, 5, 11	cmpt 4729	. . 3 class ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) )
13	2, 3, 12	cmpt 4729	. 2 class ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )
14	1, 13	wceq 1483	1 wff coe1 = ( f e. _V |-> ( n e. NN0 |-> ( f ` ( 1o X. { n } ) ) ) )

This definition is referenced by:  coe1fval  19575