Theorem ply0

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

	Ref	Expression
Assertion	ply0	⊢ ( 𝑆 ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
2		id	⊢ ( 𝑆 ⊆ ℂ → 𝑆 ⊆ ℂ )
3		0cnd	⊢ ( 𝑆 ⊆ ℂ → 0 ∈ ℂ )
4	3	snssd	⊢ ( 𝑆 ⊆ ℂ → { 0 } ⊆ ℂ )
5	2 4	unssd	⊢ ( 𝑆 ⊆ ℂ → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
6		ssun2	⊢ { 0 } ⊆ ( 𝑆 ∪ { 0 } )
7		c0ex	⊢ 0 ∈ V
8	7	snss	⊢ ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) )
9	6 8	mpbir	⊢ 0 ∈ ( 𝑆 ∪ { 0 } )
10		plyconst	⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ 0 ∈ ( 𝑆 ∪ { 0 } ) ) → ( ℂ × { 0 } ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
11	5 9 10	sylancl	⊢ ( 𝑆 ⊆ ℂ → ( ℂ × { 0 } ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
12	1 11	eqeltrid	⊢ ( 𝑆 ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
13		plyun0	⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )
14	12 13	eleqtrdi	⊢ ( 𝑆 ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ 𝑆 ) )