Metamath Proof Explorer

Theorem mzpproj

Description: A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpproj ⊢V∈V∧X∈V→g∈ℤV⟼g⁡X∈mzPoly⁡V

Proof

Step Hyp Ref Expression
1 mzpincl ⊢V∈V→mzPoly⁡V∈mzPolyCld⁡V
2 mzpcl2 ⊢mzPoly⁡V∈mzPolyCld⁡V∧X∈V→g∈ℤV⟼g⁡X∈mzPoly⁡V
3 1 2 sylan ⊢V∈V∧X∈V→g∈ℤV⟼g⁡X∈mzPoly⁡V