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 ) ) |