# Metamath Proof Explorer

## Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 plybss ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {S}\subseteq ℂ$
2 plyval ${⊢}{S}\subseteq ℂ\to \mathrm{Poly}\left({S}\right)=\left\{{f}|\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\}$
3 2 eleq2d ${⊢}{S}\subseteq ℂ\to \left({F}\in \mathrm{Poly}\left({S}\right)↔{F}\in \left\{{f}|\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\}\right)$
4 id ${⊢}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
5 cnex ${⊢}ℂ\in \mathrm{V}$
6 5 mptex ${⊢}\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\in \mathrm{V}$
7 4 6 eqeltrdi ${⊢}{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to {F}\in \mathrm{V}$
8 7 a1i ${⊢}\left({n}\in {ℕ}_{0}\wedge {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\right)\to \left({F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to {F}\in \mathrm{V}\right)$
9 8 rexlimivv ${⊢}\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}\in \mathrm{V}$
10 eqeq1 ${⊢}{f}={F}\to \left({f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)↔{F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
11 10 2rexbidv ${⊢}{f}={F}\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)↔\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)$
12 9 11 elab3 ${⊢}{F}\in \left\{{f}|\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\}↔\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)$
13 3 12 syl6bb ${⊢}{S}\subseteq ℂ\to \left({F}\in \mathrm{Poly}\left({S}\right)↔\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)$
14 1 13 biadanii ${⊢}{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)$