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