Definition df-coe 21543

Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)

Assertion

Ref	Expression
df-coe	|- coeff = ( f e. (Poly ` CC ) |-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )

Distinct variable group:   f, a, k, n, z

Detailed syntax breakdown of Definition df-coe

Step	Hyp	Ref	Expression
1		ccoe 21539	. 2 class coeff
2		vf	. . 3 setvar f
3		cc 9268	. . . 4 class CC
4		cply 21537	. . . 4 class Poly
5	3, 4	cfv 5406	. . 3 class (Poly ` CC )
6		va	. . . . . . . . 9 setvar a
7	6	cv 1361	. . . . . . . 8 class a
8		vn	. . . . . . . . . . 11 setvar n
9	8	cv 1361	. . . . . . . . . 10 class n
10		c1 9271	. . . . . . . . . 10 class 1
11		caddc 9273	. . . . . . . . . 10 class +
12	9, 10, 11	co 6080	. . . . . . . . 9 class ( n + 1 )
13		cuz 10849	. . . . . . . . 9 class ZZ>=
14	12, 13	cfv 5406	. . . . . . . 8 class ( ZZ>= ` ( n + 1 ) )
15	7, 14	cima 4830	. . . . . . 7 class ( a " ( ZZ>= ` ( n + 1 ) ) )
16		cc0 9270	. . . . . . . 8 class 0
17	16	csn 3865	. . . . . . 7 class { 0 }
18	15, 17	wceq 1362	. . . . . 6 wff ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 }
19	2	cv 1361	. . . . . . 7 class f
20		vz	. . . . . . . 8 setvar z
21		cfz 11424	. . . . . . . . . 10 class ...
22	16, 9, 21	co 6080	. . . . . . . . 9 class ( 0 ... n )
23		vk	. . . . . . . . . . . 12 setvar k
24	23	cv 1361	. . . . . . . . . . 11 class k
25	24, 7	cfv 5406	. . . . . . . . . 10 class ( a ` k )
26	20	cv 1361	. . . . . . . . . . 11 class z
27		cexp 11849	. . . . . . . . . . 11 class ^
28	26, 24, 27	co 6080	. . . . . . . . . 10 class ( z ^ k )
29		cmul 9275	. . . . . . . . . 10 class x.
30	25, 28, 29	co 6080	. . . . . . . . 9 class ( ( a ` k ) x. ( z ^ k ) )
31	22, 30, 23	csu 13147	. . . . . . . 8 class sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) )
32	20, 3, 31	cmpt 4338	. . . . . . 7 class ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
33	19, 32	wceq 1362	. . . . . 6 wff f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
34	18, 33	wa 369	. . . . 5 wff ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
35		cn0 10567	. . . . 5 class NN0
36	34, 8, 35	wrex 2706	. . . 4 wff E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
37		cmap 7202	. . . . 5 class ^m
38	3, 35, 37	co 6080	. . . 4 class ( CC ^m NN0 )
39	36, 6, 38	crio 6038	. . 3 class ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
40	2, 5, 39	cmpt 4338	. 2 class ( f e. (Poly ` CC ) |-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
41	1, 40	wceq 1362	1 wff coeff = ( f e. (Poly ` CC ) |-> ( iota_ a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )

This definition is referenced by:  coeval  21576