Metamath Proof Explorer

Theorem coeidlem

Description: Lemma for coeid . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 
|- A = ( coeff ` F )
dgrub.2 
|- N = ( deg ` F )
coeid.3 
|- ( ph -> F e. ( Poly ` S ) )
coeid.4 
|- ( ph -> M e. NN0 )
coeid.5 
|- ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )
coeid.6 
|- ( ph -> ( B " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
coeid.7 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) ) )
Assertion coeidlem 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1 
 |-  A = ( coeff ` F )
2 dgrub.2 
 |-  N = ( deg ` F )
3 coeid.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 coeid.4 
 |-  ( ph -> M e. NN0 )
5 coeid.5 
 |-  ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )
6 coeid.6 
 |-  ( ph -> ( B " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
7 coeid.7 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) ) )
8 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
9 3 8 syl 
 |-  ( ph -> S C_ CC )
10 0cnd 
 |-  ( ph -> 0 e. CC )
11 10 snssd 
 |-  ( ph -> { 0 } C_ CC )
12 9 11 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
13 cnex 
 |-  CC e. _V
14 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
15 12 13 14 sylancl 
 |-  ( ph -> ( S u. { 0 } ) e. _V )
16 nn0ex 
 |-  NN0 e. _V
17 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
18 15 16 17 sylancl 
 |-  ( ph -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
19 5 18 mpbid 
 |-  ( ph -> B : NN0 --> ( S u. { 0 } ) )
20 19 12 fssd 
 |-  ( ph -> B : NN0 --> CC )
21 3 4 20 6 7 coeeq 
 |-  ( ph -> ( coeff ` F ) = B )
22 1 21 eqtr2id 
 |-  ( ph -> B = A )
23 22 adantr 
 |-  ( ( ph /\ z e. CC ) -> B = A )
24 fveq1 
 |-  ( B = A -> ( B ` k ) = ( A ` k ) )
25 24 oveq1d 
 |-  ( B = A -> ( ( B ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( z ^ k ) ) )
26 25 sumeq2sdv 
 |-  ( B = A -> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
27 23 26 syl 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
28 3 adantr 
 |-  ( ( ph /\ z e. CC ) -> F e. ( Poly ` S ) )
29 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
30 2 29 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
31 28 30 syl 
 |-  ( ( ph /\ z e. CC ) -> N e. NN0 )
32 31 nn0zd 
 |-  ( ( ph /\ z e. CC ) -> N e. ZZ )
33 4 adantr 
 |-  ( ( ph /\ z e. CC ) -> M e. NN0 )
34 33 nn0zd 
 |-  ( ( ph /\ z e. CC ) -> M e. ZZ )
35 23 imaeq1d 
 |-  ( ( ph /\ z e. CC ) -> ( B " ( ZZ>= ` ( M + 1 ) ) ) = ( A " ( ZZ>= ` ( M + 1 ) ) ) )
36 6 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( B " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
37 35 36 eqtr3d 
 |-  ( ( ph /\ z e. CC ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
38 1 2 dgrlb 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N <_ M )
39 28 33 37 38 syl3anc 
 |-  ( ( ph /\ z e. CC ) -> N <_ M )
40 eluz2 
 |-  ( M e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ M e. ZZ /\ N <_ M ) )
41 32 34 39 40 syl3anbrc 
 |-  ( ( ph /\ z e. CC ) -> M e. ( ZZ>= ` N ) )
42 fzss2 
 |-  ( M e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... M ) )
43 41 42 syl 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) C_ ( 0 ... M ) )
44 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
45 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
46 45 3 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
47 1 coef3 
 |-  ( F e. ( Poly ` CC ) -> A : NN0 --> CC )
48 46 47 syl 
 |-  ( ph -> A : NN0 --> CC )
49 48 adantr 
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
50 49 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
51 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
52 51 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
53 50 52 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
54 44 53 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
55 eldifn 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> -. k e. ( 0 ... N ) )
56 55 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> -. k e. ( 0 ... N ) )
57 eldifi 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. ( 0 ... M ) )
58 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
59 57 58 syl 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. NN0 )
60 1 2 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 /\ ( A ` k ) =/= 0 ) -> k <_ N )
61 60 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
62 28 59 61 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
63 elfzuz 
 |-  ( k e. ( 0 ... M ) -> k e. ( ZZ>= ` 0 ) )
64 57 63 syl 
 |-  ( k e. ( ( 0 ... M ) \ ( 0 ... N ) ) -> k e. ( ZZ>= ` 0 ) )
65 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
66 64 32 65 syl2anr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
67 62 66 sylibrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) =/= 0 -> k e. ( 0 ... N ) ) )
68 67 necon1bd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( -. k e. ( 0 ... N ) -> ( A ` k ) = 0 ) )
69 56 68 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( A ` k ) = 0 )
70 69 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
71 simpr 
 |-  ( ( ph /\ z e. CC ) -> z e. CC )
72 71 59 51 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( z ^ k ) e. CC )
73 72 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
74 70 73 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... M ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
75 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) e. Fin )
76 43 54 74 75 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
77 27 76 eqtr4d 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) )
78 77 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( B ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
79 7 78 eqtrd 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )