Theorem plyssc

Description: Every polynomial ring is contained in the ring of polynomials over CC . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \mathrm{Poly}\left(ℂ\right)$$
2		sseq1	$$⊢\mathrm{Poly}\left(S\right)=\varnothing \to \left(\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)\leftrightarrow \varnothing \subseteq \mathrm{Poly}\left(ℂ\right)\right)$$
3	1 2	mpbiri	$$⊢\mathrm{Poly}\left(S\right)=\varnothing \to \mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
4		n0	$$⊢\mathrm{Poly}\left(S\right)\ne \varnothing \leftrightarrow \exists ff\in \mathrm{Poly}\left(S\right)$$
5		plybss	$$⊢f\in \mathrm{Poly}\left(S\right)\to S\subseteq ℂ$$
6		ssid	$$⊢ℂ\subseteq ℂ$$
7		plyss	$$⊢\left(S\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
8	5 6 7	sylancl	$$⊢f\in \mathrm{Poly}\left(S\right)\to \mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
9	8	exlimiv	$$⊢\exists ff\in \mathrm{Poly}\left(S\right)\to \mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
10	4 9	sylbi	$$⊢\mathrm{Poly}\left(S\right)\ne \varnothing \to \mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
11	3 10	pm2.61ine	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$