Theorem ply0

Description: The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	ply0	$$⊢S\subseteq ℂ\to 0_{𝑝}\in \mathrm{Poly}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$
2		id	$$⊢S\subseteq ℂ\to S\subseteq ℂ$$
3		0cnd	$$⊢S\subseteq ℂ\to 0\in ℂ$$
4	3	snssd	$$⊢S\subseteq ℂ\to \left\{0\right\}\subseteq ℂ$$
5	2 4	unssd	$$⊢S\subseteq ℂ\to S\cup \left\{0\right\}\subseteq ℂ$$
6		ssun2	$$⊢\left\{0\right\}\subseteq S\cup \left\{0\right\}$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8	7	snss	$$⊢0\in \left(S\cup \left\{0\right\}\right)\leftrightarrow \left\{0\right\}\subseteq S\cup \left\{0\right\}$$
9	6 8	mpbir	$$⊢0\in \left(S\cup \left\{0\right\}\right)$$
10		plyconst	$$⊢\left(S\cup \left\{0\right\}\subseteq ℂ\wedge 0\in \left(S\cup \left\{0\right\}\right)\right)\to ℂ\times \left\{0\right\}\in \mathrm{Poly}\left(S\cup \left\{0\right\}\right)$$
11	5 9 10	sylancl	$$⊢S\subseteq ℂ\to ℂ\times \left\{0\right\}\in \mathrm{Poly}\left(S\cup \left\{0\right\}\right)$$
12	1 11	eqeltrid	$$⊢S\subseteq ℂ\to 0_{𝑝}\in \mathrm{Poly}\left(S\cup \left\{0\right\}\right)$$
13		plyun0	$$⊢\mathrm{Poly}\left(S\cup \left\{0\right\}\right)=\mathrm{Poly}\left(S\right)$$
14	12 13	eleqtrdi	$$⊢S\subseteq ℂ\to 0_{𝑝}\in \mathrm{Poly}\left(S\right)$$