Theorem mzpconst

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

	Ref	Expression
Assertion	mzpconst	⊢ ( ( 𝑉 ∈ V ∧ 𝐶 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐶 } ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mzpincl	⊢ ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) )
2		mzpcl1	⊢ ( ( ( mzPoly ‘ 𝑉 ) ∈ ( mzPolyCld ‘ 𝑉 ) ∧ 𝐶 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐶 } ) ∈ ( mzPoly ‘ 𝑉 ) )
3	1 2	sylan	⊢ ( ( 𝑉 ∈ V ∧ 𝐶 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐶 } ) ∈ ( mzPoly ‘ 𝑉 ) )