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 45 raleqdv
 |-  ( ( ( 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 <-> A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
47 43 46 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. ( `' A " ( CC \ { 0 } ) ) x <_ n )
48 47 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 ) )
49 48 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 ) ) )
50 49 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 ) )
51 50 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 ) )
52 3 51 mpd
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
53 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 ) )
54 29 52 53 mpsyl
 |-  ( F e. ( Poly ` S ) -> E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
55 28 54 jca
 |-  ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )