Definition df-coe 22672

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 22668	. 2 class coeff
2		vf	. . 3 setvar f
3		cc 9401	. . . 4 class CC
4		cply 22666	. . . 4 class Poly
5	3, 4	cfv 5496	. . 3 class (Poly ` CC )
6		va	. . . . . . . . 9 setvar a
7	6	cv 1398	. . . . . . . 8 class a
8		vn	. . . . . . . . . . 11 setvar n
9	8	cv 1398	. . . . . . . . . 10 class n
10		c1 9404	. . . . . . . . . 10 class 1
11		caddc 9406	. . . . . . . . . 10 class +
12	9, 10, 11	co 6196	. . . . . . . . 9 class ( n + 1 )
13		cuz 11001	. . . . . . . . 9 class ZZ>=
14	12, 13	cfv 5496	. . . . . . . 8 class ( ZZ>= ` ( n + 1 ) )
15	7, 14	cima 4916	. . . . . . 7 class ( a " ( ZZ>= ` ( n + 1 ) ) )
16		cc0 9403	. . . . . . . 8 class 0
17	16	csn 3944	. . . . . . 7 class { 0 }
18	15, 17	wceq 1399	. . . . . 6 wff ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 }
19	2	cv 1398	. . . . . . 7 class f
20		vz	. . . . . . . 8 setvar z
21		cfz 11593	. . . . . . . . . 10 class ...
22	16, 9, 21	co 6196	. . . . . . . . 9 class ( 0 ... n )
23		vk	. . . . . . . . . . . 12 setvar k
24	23	cv 1398	. . . . . . . . . . 11 class k
25	24, 7	cfv 5496	. . . . . . . . . 10 class ( a ` k )
26	20	cv 1398	. . . . . . . . . . 11 class z
27		cexp 12069	. . . . . . . . . . 11 class ^
28	26, 24, 27	co 6196	. . . . . . . . . 10 class ( z ^ k )
29		cmul 9408	. . . . . . . . . 10 class x.
30	25, 28, 29	co 6196	. . . . . . . . 9 class ( ( a ` k ) x. ( z ^ k ) )
31	22, 30, 23	csu 13510	. . . . . . . 8 class sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) )
32	20, 3, 31	cmpt 4425	. . . . . . 7 class ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
33	19, 32	wceq 1399	. . . . . 6 wff f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
34	18, 33	wa 367	. . . . 5 wff ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
35		cn0 10712	. . . . 5 class NN0
36	34, 8, 35	wrex 2733	. . . 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 7338	. . . . 5 class ^m
38	3, 35, 37	co 6196	. . . 4 class ( CC ^m NN0 )
39	36, 6, 38	crio 6157	. . 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 4425	. 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 1399	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  22705