Metamath Proof Explorer

Theorem plyf

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

Ref Expression
Assertion plyf ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 elply ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
2 1 simprbi ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
3 fzfid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑛 ) ∈ Fin )
4 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
5 0cnd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0 ∈ ℂ )
6 5 snssd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → { 0 } ⊆ ℂ )
7 4 6 unssd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
8 7 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
9 8 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
10 simplrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
11 cnex ⊢ ℂ ∈ V
12 ssexg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
13 8 11 12 sylancl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑆 ∪ { 0 } ) ∈ V )
14 nn0ex ⊢ ℕ0 ∈ V
15 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
16 13 14 15 sylancl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
17 10 16 mpbid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
18 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
19 ffvelcdm ⊢ ( ( 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
20 17 18 19 syl2an ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
21 9 20 sseldd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎 ‘ 𝑘 ) ∈ ℂ )
22 simpr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
23 expcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
24 22 18 23 syl2an ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
25 21 24 mulcld ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
26 3 25 fsumcl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
27 26 fmpttd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) : ℂ ⟶ ℂ )
28 feq1 ⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( 𝐹 : ℂ ⟶ ℂ ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) : ℂ ⟶ ℂ ) )
29 27 28 syl5ibrcom ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 : ℂ ⟶ ℂ ) )
30 29 rexlimdvva ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 : ℂ ⟶ ℂ ) )
31 2 30 mpd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )