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 ℂ\leftrightarrow \left(S\subseteq ℂ\wedge \left\{0\right\}\subseteq ℂ\right)$$
5		unss	$$⊢\left(S\subseteq ℂ\wedge \left\{0\right\}\subseteq ℂ\right)\leftrightarrow S\cup \left\{0\right\}\subseteq ℂ$$
6	4 5	bitr2i	$$⊢S\cup \left\{0\right\}\subseteq ℂ\leftrightarrow 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)}^{{\mathbb{N}}_0}={\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}$$
12	11	rexeqi	$$⊢\exists a\in \left({\left(\left(S\cup \left\{0\right\}\right)\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow \exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
13	12	rexbii	$$⊢\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(\left(S\cup \left\{0\right\}\right)\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)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 {\mathbb{N}}_0\exists a\in \left({\left(\left(S\cup \left\{0\right\}\right)\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \left(S\subseteq ℂ\wedge \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)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)\leftrightarrow \left(S\cup \left\{0\right\}\subseteq ℂ\wedge \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(\left(S\cup \left\{0\right\}\right)\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)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)\leftrightarrow \left(S\subseteq ℂ\wedge \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)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)\leftrightarrow f\in \mathrm{Poly}\left(S\right)$$
18	17	eqriv	$$⊢\mathrm{Poly}\left(S\cup \left\{0\right\}\right)=\mathrm{Poly}\left(S\right)$$