Metamath Proof Explorer

Theorem gg-plycn

Description: A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Assertion gg-plycn ⊢F∈Poly⁡S→F:ℂ⟶cnℂ

Proof

Step Hyp Ref Expression
1 eqid ⊢coeff⁡F=coeff⁡F
2 eqid ⊢deg⁡F=deg⁡F
3 1 2 coeid ⊢F∈Poly⁡S→F=z∈ℂ⟼∑k=0deg⁡Fcoeff⁡F⁡k⁢zk
4 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
5 4 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
6 5 a1i ⊢F∈Poly⁡S→TopOpen⁡ℂfld∈TopOn⁡ℂ
7 fzfid ⊢F∈Poly⁡S→0…deg⁡F∈Fin
8 5 a1i ⊢F∈Poly⁡S∧k∈0…deg⁡F→TopOpen⁡ℂfld∈TopOn⁡ℂ
9 1 coef3 ⊢F∈Poly⁡S→coeff⁡F:ℕ0⟶ℂ
10 elfznn0 ⊢k∈0…deg⁡F→k∈ℕ0
11 ffvelcdm ⊢coeff⁡F:ℕ0⟶ℂ∧k∈ℕ0→coeff⁡F⁡k∈ℂ
12 9 10 11 syl2an ⊢F∈Poly⁡S∧k∈0…deg⁡F→coeff⁡F⁡k∈ℂ
13 8 8 12 cnmptc ⊢F∈Poly⁡S∧k∈0…deg⁡F→z∈ℂ⟼coeff⁡F⁡k∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
14 10 adantl ⊢F∈Poly⁡S∧k∈0…deg⁡F→k∈ℕ0
15 4 gg-expcn ⊢k∈ℕ0→z∈ℂ⟼zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
16 14 15 syl ⊢F∈Poly⁡S∧k∈0…deg⁡F→z∈ℂ⟼zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
17 4 mpomulcn ⊢u∈ℂ,v∈ℂ⟼u⁢v∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 17 a1i ⊢F∈Poly⁡S∧k∈0…deg⁡F→u∈ℂ,v∈ℂ⟼u⁢v∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
19 oveq12 ⊢u=coeff⁡F⁡k∧v=zk→u⁢v=coeff⁡F⁡k⁢zk
20 8 13 16 8 8 18 19 cnmpt12 ⊢F∈Poly⁡S∧k∈0…deg⁡F→z∈ℂ⟼coeff⁡F⁡k⁢zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
21 4 6 7 20 fsumcn ⊢F∈Poly⁡S→z∈ℂ⟼∑k=0deg⁡Fcoeff⁡F⁡k⁢zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
22 3 21 eqeltrd ⊢F∈Poly⁡S→F∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
23 4 cncfcn1 ⊢ℂ⟶cnℂ=TopOpen⁡ℂfldCnTopOpen⁡ℂfld
24 22 23 eleqtrrdi ⊢F∈Poly⁡S→F:ℂ⟶cnℂ