# Metamath Proof Explorer

## 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)↔\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 ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\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 {f}\phantom{\rule{.4em}{0ex}}{f}\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)$