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 ) )