Metamath Proof Explorer

Theorem plycn

Description: A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion plycn 
|- ( F e. ( Poly ` S ) -> F e. ( CC -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
2 eqid 
 |-  ( deg ` F ) = ( deg ` F )
3 1 2 coeid 
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) )
4 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
5 4 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
6 5 a1i 
 |-  ( F e. ( Poly ` S ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
7 fzfid 
 |-  ( F e. ( Poly ` S ) -> ( 0 ... ( deg ` F ) ) e. Fin )
8 5 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
9 1 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
10 elfznn0 
 |-  ( k e. ( 0 ... ( deg ` F ) ) -> k e. NN0 )
11 ffvelrn 
 |-  ( ( ( coeff ` F ) : NN0 --> CC /\ k e. NN0 ) -> ( ( coeff ` F ) ` k ) e. CC )
12 9 10 11 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( coeff ` F ) ` k ) e. CC )
13 8 8 12 cnmptc 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( z e. CC |-> ( ( coeff ` F ) ` k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
14 10 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> k e. NN0 )
15 4 expcn 
 |-  ( k e. NN0 -> ( z e. CC |-> ( z ^ k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
16 14 15 syl 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( z e. CC |-> ( z ^ k ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
17 4 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
18 17 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
19 8 13 16 18 cnmpt12f 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( z e. CC |-> ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
20 4 6 7 19 fsumcn 
 |-  ( F e. ( Poly ` S ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( ( coeff ` F ) ` k ) x. ( z ^ k ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
21 3 20 eqeltrd 
 |-  ( F e. ( Poly ` S ) -> F e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
22 4 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
23 21 22 eleqtrrdi 
 |-  ( F e. ( Poly ` S ) -> F e. ( CC -cn-> CC ) )