This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ Poly ⁡ ℂ
2 sseq1 ⊢ Poly ⁡ S = ∅ → Poly ⁡ S ⊆ Poly ⁡ ℂ ↔ ∅ ⊆ Poly ⁡ ℂ
3 1 2 mpbiri ⊢ Poly ⁡ S = ∅ → Poly ⁡ S ⊆ Poly ⁡ ℂ
4 n0 ⊢ Poly ⁡ S ≠ ∅ ↔ ∃ f f ∈ Poly ⁡ S
5 plybss ⊢ f ∈ Poly ⁡ S → S ⊆ ℂ
6 ssid ⊢ ℂ ⊆ ℂ
7 plyss ⊢ S ⊆ ℂ ∧ ℂ ⊆ ℂ → Poly ⁡ S ⊆ Poly ⁡ ℂ
8 5 6 7 sylancl ⊢ f ∈ Poly ⁡ S → Poly ⁡ S ⊆ Poly ⁡ ℂ
9 8 exlimiv ⊢ ∃ f f ∈ Poly ⁡ S → Poly ⁡ S ⊆ Poly ⁡ ℂ
10 4 9 sylbi ⊢ Poly ⁡ S ≠ ∅ → Poly ⁡ S ⊆ Poly ⁡ ℂ
11 3 10 pm2.61ine ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ