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 ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )

Proof

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