Metamath Proof Explorer

Theorem 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 plycn ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
2 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
3 1 2 coeid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
4 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
5 4 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
6 5 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
7 fzfid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
8 5 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
9 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
10 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑘 ∈ ℕ0 )
11 ffvelcdm ⊢ ( ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
12 9 10 11 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
13 8 8 12 cnmptc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
14 10 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑘 ∈ ℕ0 )
15 4 expcn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
16 14 15 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17 4 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
18 17 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
19 oveq12 ⊢ ( ( 𝑢 = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ∧ 𝑣 = ( 𝑧 ↑ 𝑘 ) ) → ( 𝑢 · 𝑣 ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
20 8 13 16 8 8 18 19 cnmpt12 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑧 ∈ ℂ ↦ ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
21 4 6 7 20 fsumcn ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
22 3 21 eqeltrd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
23 4 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
24 22 23 eleqtrrdi ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )