# Metamath Proof Explorer

## Theorem plyun0

Description: The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyun0 ${⊢}\mathrm{Poly}\left({S}\cup \left\{0\right\}\right)=\mathrm{Poly}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 0cn ${⊢}0\in ℂ$
2 snssi ${⊢}0\in ℂ\to \left\{0\right\}\subseteq ℂ$
3 1 2 ax-mp ${⊢}\left\{0\right\}\subseteq ℂ$
4 3 biantru ${⊢}{S}\subseteq ℂ↔\left({S}\subseteq ℂ\wedge \left\{0\right\}\subseteq ℂ\right)$
5 unss ${⊢}\left({S}\subseteq ℂ\wedge \left\{0\right\}\subseteq ℂ\right)↔{S}\cup \left\{0\right\}\subseteq ℂ$
6 4 5 bitr2i ${⊢}{S}\cup \left\{0\right\}\subseteq ℂ↔{S}\subseteq ℂ$
7 unass ${⊢}\left({S}\cup \left\{0\right\}\right)\cup \left\{0\right\}={S}\cup \left(\left\{0\right\}\cup \left\{0\right\}\right)$
8 unidm ${⊢}\left\{0\right\}\cup \left\{0\right\}=\left\{0\right\}$
9 8 uneq2i ${⊢}{S}\cup \left(\left\{0\right\}\cup \left\{0\right\}\right)={S}\cup \left\{0\right\}$
10 7 9 eqtri ${⊢}\left({S}\cup \left\{0\right\}\right)\cup \left\{0\right\}={S}\cup \left\{0\right\}$
11 10 oveq1i ${⊢}{\left(\left({S}\cup \left\{0\right\}\right)\cup \left\{0\right\}\right)}^{{ℕ}_{0}}={\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}$
12 11 rexeqi ${⊢}\exists {a}\in \left({\left(\left({S}\cup \left\{0\right\}\right)\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 {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 12 rexbii ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left(\left({S}\cup \left\{0\right\}\right)\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)$
14 6 13 anbi12i ${⊢}\left({S}\cup \left\{0\right\}\subseteq ℂ\wedge \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left(\left({S}\cup \left\{0\right\}\right)\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)↔\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)$
15 elply ${⊢}{f}\in \mathrm{Poly}\left({S}\cup \left\{0\right\}\right)↔\left({S}\cup \left\{0\right\}\subseteq ℂ\wedge \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left(\left({S}\cup \left\{0\right\}\right)\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)$
16 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)$
17 14 15 16 3bitr4i ${⊢}{f}\in \mathrm{Poly}\left({S}\cup \left\{0\right\}\right)↔{f}\in \mathrm{Poly}\left({S}\right)$
18 17 eqriv ${⊢}\mathrm{Poly}\left({S}\cup \left\{0\right\}\right)=\mathrm{Poly}\left({S}\right)$