Theorem mzpconstmpt

Description: A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow ( mzpaddmpt , mzpmulmpt , mzpnegmpt , mzpsubmpt , mzpexpmpt ) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014)

	Ref	Expression
Assertion	mzpconstmpt	⊢ ( ( 𝑉 ∈ V ∧ 𝐶 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐶 ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	⊢ ( ( ℤ ↑m 𝑉 ) × { 𝐶 } ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐶 )
2		mzpconst	⊢ ( ( 𝑉 ∈ V ∧ 𝐶 ∈ ℤ ) → ( ( ℤ ↑m 𝑉 ) × { 𝐶 } ) ∈ ( mzPoly ‘ 𝑉 ) )
3	1 2	eqeltrrid	⊢ ( ( 𝑉 ∈ V ∧ 𝐶 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐶 ) ∈ ( mzPoly ‘ 𝑉 ) )