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