# Metamath Proof Explorer

## 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 ${⊢}\left({V}\in \mathrm{V}\wedge {C}\in ℤ\right)\to \left({x}\in \left({ℤ}^{{V}}\right)⟼{C}\right)\in \mathrm{mzPoly}\left({V}\right)$

### Proof

Step Hyp Ref Expression
1 fconstmpt ${⊢}\left({ℤ}^{{V}}\right)×\left\{{C}\right\}=\left({x}\in \left({ℤ}^{{V}}\right)⟼{C}\right)$
2 mzpconst ${⊢}\left({V}\in \mathrm{V}\wedge {C}\in ℤ\right)\to \left({ℤ}^{{V}}\right)×\left\{{C}\right\}\in \mathrm{mzPoly}\left({V}\right)$
3 1 2 eqeltrrid ${⊢}\left({V}\in \mathrm{V}\wedge {C}\in ℤ\right)\to \left({x}\in \left({ℤ}^{{V}}\right)⟼{C}\right)\in \mathrm{mzPoly}\left({V}\right)$