Metamath Proof Explorer

Theorem plyf

Description: The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion plyf 
|- ( F e. ( Poly ` S ) -> F : CC --> CC )

Proof

Step Hyp Ref Expression
1 elply 
 |-  ( F e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
2 1 simprbi 
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
3 fzfid 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( 0 ... n ) e. Fin )
4 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
5 0cnd 
 |-  ( F e. ( Poly ` S ) -> 0 e. CC )
6 5 snssd 
 |-  ( F e. ( Poly ` S ) -> { 0 } C_ CC )
7 4 6 unssd 
 |-  ( F e. ( Poly ` S ) -> ( S u. { 0 } ) C_ CC )
8 7 ad2antrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( S u. { 0 } ) C_ CC )
9 8 adantr 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( S u. { 0 } ) C_ CC )
10 simplrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> a e. ( ( S u. { 0 } ) ^m NN0 ) )
11 cnex 
 |-  CC e. _V
12 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
13 8 11 12 sylancl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( 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 ) ) ) /\ z e. CC ) -> ( a e. ( ( S u. { 0 } ) ^m NN0 ) <-> a : NN0 --> ( S u. { 0 } ) ) )
17 10 16 mpbid 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> a : NN0 --> ( S u. { 0 } ) )
18 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
19 ffvelrn 
 |-  ( ( a : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( a ` k ) e. ( S u. { 0 } ) )
20 17 18 19 syl2an 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. ( S u. { 0 } ) )
21 9 20 sseldd 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. CC )
22 simpr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> z e. CC )
23 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
24 22 18 23 syl2an 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( z ^ k ) e. CC )
25 21 24 mulcld 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( ( a ` k ) x. ( z ^ k ) ) e. CC )
26 3 25 fsumcl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) e. CC )
27 26 fmpttd 
 |-  ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) : CC --> CC )
28 feq1 
 |-  ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> ( F : CC --> CC <-> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) : CC --> CC ) )
29 27 28 syl5ibrcom 
 |-  ( ( F e. ( Poly ` S ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> F : CC --> CC ) )
30 29 rexlimdvva 
 |-  ( F e. ( Poly ` S ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> F : CC --> CC ) )
31 2 30 mpd 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )