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

Metamath Proof Explorer

Theorem ply0

Description: The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion ply0 
|- ( S C_ CC -> 0p e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 df-0p 
 |-  0p = ( CC X. { 0 } )
2 id 
 |-  ( S C_ CC -> S C_ CC )
3 0cnd 
 |-  ( S C_ CC -> 0 e. CC )
4 3 snssd 
 |-  ( S C_ CC -> { 0 } C_ CC )
5 2 4 unssd 
 |-  ( S C_ CC -> ( S u. { 0 } ) C_ CC )
6 ssun2 
 |-  { 0 } C_ ( S u. { 0 } )
7 c0ex 
 |-  0 e. _V
8 7 snss 
 |-  ( 0 e. ( S u. { 0 } ) <-> { 0 } C_ ( S u. { 0 } ) )
9 6 8 mpbir 
 |-  0 e. ( S u. { 0 } )
10 plyconst 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ 0 e. ( S u. { 0 } ) ) -> ( CC X. { 0 } ) e. ( Poly ` ( S u. { 0 } ) ) )
11 5 9 10 sylancl 
 |-  ( S C_ CC -> ( CC X. { 0 } ) e. ( Poly ` ( S u. { 0 } ) ) )
12 1 11 eqeltrid 
 |-  ( S C_ CC -> 0p e. ( Poly ` ( S u. { 0 } ) ) )
13 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
14 12 13 eleqtrdi 
 |-  ( S C_ CC -> 0p e. ( Poly ` S ) )