# 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 ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}:ℂ⟶ℂ$

### Proof

Step Hyp Ref Expression
1 elply ${⊢}{F}\in \mathrm{Poly}\left({S}\right)↔\left({S}\subseteq ℂ\wedge \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
2 1 simprbi ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
3 fzfid ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to \left(0\dots {n}\right)\in \mathrm{Fin}$
4 plybss ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {S}\subseteq ℂ$
5 0cnd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to 0\in ℂ$
6 5 snssd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left\{0\right\}\subseteq ℂ$
7 4 6 unssd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {S}\cup \left\{0\right\}\subseteq ℂ$
8 7 ad2antrr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to {S}\cup \left\{0\right\}\subseteq ℂ$
9 8 adantr ${⊢}\left(\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {S}\cup \left\{0\right\}\subseteq ℂ$
10 simplrr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
11 cnex ${⊢}ℂ\in \mathrm{V}$
12 ssexg ${⊢}\left({S}\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {S}\cup \left\{0\right\}\in \mathrm{V}$
13 8 11 12 sylancl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to {S}\cup \left\{0\right\}\in \mathrm{V}$
14 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
15 elmapg ${⊢}\left({S}\cup \left\{0\right\}\in \mathrm{V}\wedge {ℕ}_{0}\in \mathrm{V}\right)\to \left({a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{a}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
16 13 14 15 sylancl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to \left({a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{a}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
17 10 16 mpbid ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to {a}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
18 elfznn0 ${⊢}{k}\in \left(0\dots {n}\right)\to {k}\in {ℕ}_{0}$
19 ffvelrn ${⊢}\left({a}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\wedge {k}\in {ℕ}_{0}\right)\to {a}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)$
20 17 18 19 syl2an ${⊢}\left(\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {a}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)$
21 9 20 sseldd ${⊢}\left(\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {a}\left({k}\right)\in ℂ$
22 simpr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to {z}\in ℂ$
23 expcl ${⊢}\left({z}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{z}}^{{k}}\in ℂ$
24 22 18 23 syl2an ${⊢}\left(\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {{z}}^{{k}}\in ℂ$
25 21 24 mulcld ${⊢}\left(\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {a}\left({k}\right){{z}}^{{k}}\in ℂ$
26 3 25 fsumcl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\in ℂ$
27 26 fmpttd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right):ℂ⟶ℂ$
28 feq1 ${⊢}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to \left({F}:ℂ⟶ℂ↔\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right):ℂ⟶ℂ\right)$
29 27 28 syl5ibrcom ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge \left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\right)\to \left({F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to {F}:ℂ⟶ℂ\right)$
30 29 rexlimdvva ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to {F}:ℂ⟶ℂ\right)$
31 2 30 mpd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}:ℂ⟶ℂ$