Metamath Proof Explorer

Definition df-coe

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

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoe 
 |-  coeff
1 vf 
 |-  f
2 cply 
 |-  Poly
3 cc 
 |-  CC
4 3 2 cfv 
 |-  ( Poly ` CC )
5 va 
 |-  a
6 cmap 
 |-  ^m
7 cn0 
 |-  NN0
8 3 7 6 co 
 |-  ( CC ^m NN0 )
9 vn 
 |-  n
10 5 cv 
 |-  a
11 cuz 
 |-  ZZ>=
12 9 cv 
 |-  n
13 caddc 
 |-  +
14 c1 
 |-  1
15 12 14 13 co 
 |-  ( n + 1 )
16 15 11 cfv 
 |-  ( ZZ>= ` ( n + 1 ) )
17 10 16 cima 
 |-  ( a " ( ZZ>= ` ( n + 1 ) ) )
18 cc0 
 |-  0
19 18 csn 
 |-  { 0 }
20 17 19 wceq 
 |-  ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 }
21 1 cv 
 |-  f
22 vz 
 |-  z
23 vk 
 |-  k
24 cfz 
 |-  ...
25 18 12 24 co 
 |-  ( 0 ... n )
26 23 cv 
 |-  k
27 26 10 cfv 
 |-  ( a ` k )
28 cmul 
 |-  x.
29 22 cv 
 |-  z
30 cexp 
 |-  ^
31 29 26 30 co 
 |-  ( z ^ k )
32 27 31 28 co 
 |-  ( ( a ` k ) x. ( z ^ k ) )
33 25 32 23 csu 
 |-  sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) )
34 22 3 33 cmpt 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
35 21 34 wceq 
 |-  f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
36 20 35 wa 
 |-  ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
37 36 9 7 wrex 
 |-  E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
38 37 5 8 crio 
 |-  ( 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 ) ) ) ) )
39 1 4 38 cmpt 
 |-  ( 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 ) ) ) ) ) )
40 0 39 wceq 
 |-  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 ) ) ) ) ) )