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 VVCV×CmzPolyV

Proof

Step Hyp Ref Expression
1 mzpincl VVmzPolyVmzPolyCldV
2 mzpcl1 mzPolyVmzPolyCldVCV×CmzPolyV
3 1 2 sylan VVCV×CmzPolyV