Metamath Proof Explorer


Theorem plyf

Description: The 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 } ) ↑m0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
2 1 simprbi ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
3 fzfid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 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 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
9 8 adantr ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
10 simplrr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
11 cnex ℂ ∈ V
12 ssexg ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
13 8 11 12 sylancl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑆 ∪ { 0 } ) ∈ V )
14 nn0ex 0 ∈ V
15 elmapg ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
16 13 14 15 sylancl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
17 10 16 mpbid ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
18 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
19 ffvelrn ( ( 𝑎 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑎𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
20 17 18 19 syl2an ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
21 9 20 sseldd ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑎𝑘 ) ∈ ℂ )
22 simpr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
23 expcl ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧𝑘 ) ∈ ℂ )
24 22 18 23 syl2an ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧𝑘 ) ∈ ℂ )
25 21 24 mulcld ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
26 3 25 fsumcl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
27 26 fmpttd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) : ℂ ⟶ ℂ )
28 feq1 ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) → ( 𝐹 : ℂ ⟶ ℂ ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) : ℂ ⟶ ℂ ) )
29 27 28 syl5ibrcom ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ) ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) → 𝐹 : ℂ ⟶ ℂ ) )
30 29 rexlimdvva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) → 𝐹 : ℂ ⟶ ℂ ) )
31 2 30 mpd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )