Metamath Proof Explorer

Theorem dgrlem

Description: Lemma for dgrcl and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypothesis dgrval.1 
|- A = ( coeff ` F )
Assertion dgrlem 
|- ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )

Proof

Step Hyp Ref Expression
1 dgrval.1 
 |-  A = ( coeff ` F )
2 elply2 
 |-  ( F e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
3 2 simprbi 
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
4 simplrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> a e. ( ( S u. { 0 } ) ^m NN0 ) )
5 simpll 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> F e. ( Poly ` S ) )
6 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
7 5 6 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> S C_ CC )
8 0cnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> 0 e. CC )
9 8 snssd 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> { 0 } C_ CC )
10 7 9 unssd 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( S u. { 0 } ) C_ CC )
11 cnex 
 |-  CC e. _V
12 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
13 10 11 12 sylancl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( S u. { 0 } ) e. _V )
14 nn0ex 
 |-  NN0 e. _V
15 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( a e. ( ( S u. { 0 } ) ^m NN0 ) <-> a : NN0 --> ( S u. { 0 } ) ) )
16 13 14 15 sylancl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( a e. ( ( S u. { 0 } ) ^m NN0 ) <-> a : NN0 --> ( S u. { 0 } ) ) )
17 4 16 mpbid 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
18 simplrl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> n e. NN0 )
19 17 10 fssd 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> a : NN0 --> CC )
20 simprl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } )
21 simprr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
22 5 18 19 20 21 coeeq 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( coeff ` F ) = a )
23 1 22 eqtr2id 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> a = A )
24 23 feq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( a : NN0 --> ( S u. { 0 } ) <-> A : NN0 --> ( S u. { 0 } ) ) )
25 17 24 mpbid 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> A : NN0 --> ( S u. { 0 } ) )
26 25 ex 
 |-  ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> A : NN0 --> ( S u. { 0 } ) ) )
27 26 rexlimdvva 
 |-  ( F e. ( Poly ` S ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> A : NN0 --> ( S u. { 0 } ) ) )
28 3 27 mpd 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )
29 nn0ssz 
 |-  NN0 C_ ZZ
30 ffn 
 |-  ( a : NN0 --> CC -> a Fn NN0 )
31 elpreima 
 |-  ( a Fn NN0 -> ( x e. ( `' a " ( CC \ { 0 } ) ) <-> ( x e. NN0 /\ ( a ` x ) e. ( CC \ { 0 } ) ) ) )
32 19 30 31 3syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( x e. ( `' a " ( CC \ { 0 } ) ) <-> ( x e. NN0 /\ ( a ` x ) e. ( CC \ { 0 } ) ) ) )
33 32 biimpa 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. ( `' a " ( CC \ { 0 } ) ) ) -> ( x e. NN0 /\ ( a ` x ) e. ( CC \ { 0 } ) ) )
34 eldifsni 
 |-  ( ( a ` x ) e. ( CC \ { 0 } ) -> ( a ` x ) =/= 0 )
35 33 34 simpl2im 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. ( `' a " ( CC \ { 0 } ) ) ) -> ( a ` x ) =/= 0 )
36 33 simpld 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. ( `' a " ( CC \ { 0 } ) ) ) -> x e. NN0 )
37 plyco0 
 |-  ( ( n e. NN0 /\ a : NN0 --> CC ) -> ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> A. x e. NN0 ( ( a ` x ) =/= 0 -> x <_ n ) ) )
38 18 19 37 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> A. x e. NN0 ( ( a ` x ) =/= 0 -> x <_ n ) ) )
39 20 38 mpbid 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> A. x e. NN0 ( ( a ` x ) =/= 0 -> x <_ n ) )
40 39 r19.21bi 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. NN0 ) -> ( ( a ` x ) =/= 0 -> x <_ n ) )
41 36 40 syldan 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. ( `' a " ( CC \ { 0 } ) ) ) -> ( ( a ` x ) =/= 0 -> x <_ n ) )
42 35 41 mpd 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) /\ x e. ( `' a " ( CC \ { 0 } ) ) ) -> x <_ n )
43 42 ralrimiva 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> A. x e. ( `' a " ( CC \ { 0 } ) ) x <_ n )
44 23 cnveqd 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> `' a = `' A )
45 44 imaeq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> ( `' a " ( CC \ { 0 } ) ) = ( `' A " ( CC \ { 0 } ) ) )
46 43 45 raleqtrdv 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) -> A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
47 46 ex 
 |-  ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
48 47 expr 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) ) )
49 48 rexlimdv 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
50 49 reximdva 
 |-  ( F e. ( Poly ` S ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) -> E. n e. NN0 A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
51 3 50 mpd 
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
52 ssrexv 
 |-  ( NN0 C_ ZZ -> ( E. n e. NN0 A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n -> E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
53 29 51 52 mpsyl 
 |-  ( F e. ( Poly ` S ) -> E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
54 28 53 jca 
 |-  ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )