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 ) C_ ( Poly ` CC )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ ( Poly ` CC )
2 sseq1 
 |-  ( ( Poly ` S ) = (/) -> ( ( Poly ` S ) C_ ( Poly ` CC ) <-> (/) C_ ( Poly ` CC ) ) )
3 1 2 mpbiri 
 |-  ( ( Poly ` S ) = (/) -> ( Poly ` S ) C_ ( Poly ` CC ) )
4 n0 
 |-  ( ( Poly ` S ) =/= (/) <-> E. f f e. ( Poly ` S ) )
5 plybss 
 |-  ( f e. ( Poly ` S ) -> S C_ CC )
6 ssid 
 |-  CC C_ CC
7 plyss 
 |-  ( ( S C_ CC /\ CC C_ CC ) -> ( Poly ` S ) C_ ( Poly ` CC ) )
8 5 6 7 sylancl 
 |-  ( f e. ( Poly ` S ) -> ( Poly ` S ) C_ ( Poly ` CC ) )
9 8 exlimiv 
 |-  ( E. f f e. ( Poly ` S ) -> ( Poly ` S ) C_ ( Poly ` CC ) )
10 4 9 sylbi 
 |-  ( ( Poly ` S ) =/= (/) -> ( Poly ` S ) C_ ( Poly ` CC ) )
11 3 10 pm2.61ine 
 |-  ( Poly ` S ) C_ ( Poly ` CC )