Metamath Proof Explorer


Theorem coeeq2

Description: Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1
|- ( ph -> F e. ( Poly ` S ) )
dgrle.2
|- ( ph -> N e. NN0 )
dgrle.3
|- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
dgrle.4
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
Assertion coeeq2
|- ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgrle.1
 |-  ( ph -> F e. ( Poly ` S ) )
2 dgrle.2
 |-  ( ph -> N e. NN0 )
3 dgrle.3
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
4 dgrle.4
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
5 simpll
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> ph )
6 simpr
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k <_ N )
7 simplr
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. NN0 )
8 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 eleqtrdi
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. ( ZZ>= ` 0 ) )
10 2 nn0zd
 |-  ( ph -> N e. ZZ )
11 10 ad2antrr
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> N e. ZZ )
12 elfz5
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
13 9 11 12 syl2anc
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
14 6 13 mpbird
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. ( 0 ... N ) )
15 5 14 3 syl2anc
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> A e. CC )
16 0cnd
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ N ) -> 0 e. CC )
17 15 16 ifclda
 |-  ( ( ph /\ k e. NN0 ) -> if ( k <_ N , A , 0 ) e. CC )
18 17 fmpttd
 |-  ( ph -> ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) : NN0 --> CC )
19 simpr
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
20 eqid
 |-  ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) )
21 20 fvmpt2
 |-  ( ( k e. NN0 /\ if ( k <_ N , A , 0 ) e. CC ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
22 19 17 21 syl2anc
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
23 22 neeq1d
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 <-> if ( k <_ N , A , 0 ) =/= 0 ) )
24 iffalse
 |-  ( -. k <_ N -> if ( k <_ N , A , 0 ) = 0 )
25 24 necon1ai
 |-  ( if ( k <_ N , A , 0 ) =/= 0 -> k <_ N )
26 23 25 syl6bi
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
27 26 ralrimiva
 |-  ( ph -> A. k e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
28 nfv
 |-  F/ m ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N )
29 nffvmpt1
 |-  F/_ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m )
30 nfcv
 |-  F/_ k 0
31 29 30 nfne
 |-  F/ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0
32 nfv
 |-  F/ k m <_ N
33 31 32 nfim
 |-  F/ k ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N )
34 fveq2
 |-  ( k = m -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) )
35 34 neeq1d
 |-  ( k = m -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 <-> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 ) )
36 breq1
 |-  ( k = m -> ( k <_ N <-> m <_ N ) )
37 35 36 imbi12d
 |-  ( k = m -> ( ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) <-> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
38 28 33 37 cbvralw
 |-  ( A. k e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) )
39 27 38 sylib
 |-  ( ph -> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) )
40 plyco0
 |-  ( ( N e. NN0 /\ ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) : NN0 --> CC ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
41 2 18 40 syl2anc
 |-  ( ph -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
42 39 41 mpbird
 |-  ( ph -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
43 nfcv
 |-  F/_ m ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) )
44 nfcv
 |-  F/_ k x.
45 nfcv
 |-  F/_ k ( z ^ m )
46 29 44 45 nfov
 |-  F/_ k ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) )
47 oveq2
 |-  ( k = m -> ( z ^ k ) = ( z ^ m ) )
48 34 47 oveq12d
 |-  ( k = m -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) )
49 43 46 48 cbvsumi
 |-  sum_ k e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) )
50 elfznn0
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
51 50 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
52 elfzle2
 |-  ( k e. ( 0 ... N ) -> k <_ N )
53 52 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> k <_ N )
54 53 iftrued
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> if ( k <_ N , A , 0 ) = A )
55 3 adantlr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> A e. CC )
56 54 55 eqeltrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> if ( k <_ N , A , 0 ) e. CC )
57 51 56 21 syl2anc
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
58 57 54 eqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = A )
59 58 oveq1d
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( A x. ( z ^ k ) ) )
60 59 sumeq2dv
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) )
61 49 60 eqtr3id
 |-  ( ( ph /\ z e. CC ) -> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) = sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) )
62 61 mpteq2dva
 |-  ( ph -> ( z e. CC |-> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
63 4 62 eqtr4d
 |-  ( ph -> F = ( z e. CC |-> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) ) )
64 1 2 18 42 63 coeeq
 |-  ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )