Metamath Proof Explorer

Theorem mzpconst

Description: Constant functions are polynomial. See also mzpconstmpt . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpconst ⊢ V ∈ V ∧ C ∈ ℤ → ℤ V × C ∈ mzPoly ⁡ V

Proof

Step Hyp Ref Expression
1 mzpincl ⊢ V ∈ V → mzPoly ⁡ V ∈ mzPolyCld ⁡ V
2 mzpcl1 ⊢ mzPoly ⁡ V ∈ mzPolyCld ⁡ V ∧ C ∈ ℤ → ℤ V × C ∈ mzPoly ⁡ V
3 1 2 sylan ⊢ V ∈ V ∧ C ∈ ℤ → ℤ V × C ∈ mzPoly ⁡ V