# Metamath Proof Explorer

## Theorem elplyr

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion elplyr ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\in \mathrm{Poly}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {S}\subseteq ℂ$
2 simp2 ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {N}\in {ℕ}_{0}$
3 simp3 ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {A}:{ℕ}_{0}⟶{S}$
4 ssun1 ${⊢}{S}\subseteq {S}\cup \left\{0\right\}$
5 fss ${⊢}\left({A}:{ℕ}_{0}⟶{S}\wedge {S}\subseteq {S}\cup \left\{0\right\}\right)\to {A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
6 3 4 5 sylancl ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
7 0cnd ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to 0\in ℂ$
8 7 snssd ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to \left\{0\right\}\subseteq ℂ$
9 1 8 unssd ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {S}\cup \left\{0\right\}\subseteq ℂ$
10 cnex ${⊢}ℂ\in \mathrm{V}$
11 ssexg ${⊢}\left({S}\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {S}\cup \left\{0\right\}\in \mathrm{V}$
12 9 10 11 sylancl ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {S}\cup \left\{0\right\}\in \mathrm{V}$
13 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
14 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)$
15 12 13 14 sylancl ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to \left({A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
16 6 15 mpbird ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to {A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
17 eqidd ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)$
18 oveq2 ${⊢}{n}={N}\to \left(0\dots {n}\right)=\left(0\dots {N}\right)$
19 18 sumeq1d ${⊢}{n}={N}\to \sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}$
20 19 mpteq2dv ${⊢}{n}={N}\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}\right)$
21 20 eqeq2d ${⊢}{n}={N}\to \left(\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)↔\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
22 fveq1 ${⊢}{a}={A}\to {a}\left({k}\right)={A}\left({k}\right)$
23 22 oveq1d ${⊢}{a}={A}\to {a}\left({k}\right){{z}}^{{k}}={A}\left({k}\right){{z}}^{{k}}$
24 23 sumeq2sdv ${⊢}{a}={A}\to \sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}=\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}$
25 24 mpteq2dv ${⊢}{a}={A}\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)$
26 25 eqeq2d ${⊢}{a}={A}\to \left(\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{a}\left({k}\right){{z}}^{{k}}\right)↔\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\right)$
27 21 26 rspc2ev ${⊢}\left({N}\in {ℕ}_{0}\wedge {A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\wedge \left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\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}}\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
28 2 16 17 27 syl3anc ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{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}}\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)$
29 elply ${⊢}\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\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}}\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
30 1 28 29 sylanbrc ${⊢}\left({S}\subseteq ℂ\wedge {N}\in {ℕ}_{0}\wedge {A}:{ℕ}_{0}⟶{S}\right)\to \left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{z}}^{{k}}\right)\in \mathrm{Poly}\left({S}\right)$