Theorem mzpproj

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

	Ref	Expression
Assertion	mzpproj	|- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. ( mzPoly ` V ) )

Proof

Step	Hyp	Ref	Expression
1		mzpincl	|- ( V e. _V -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) )
2		mzpcl2	|- ( ( ( mzPoly ` V ) e. ( mzPolyCld ` V ) /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. ( mzPoly ` V ) )
3	1 2	sylan	|- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. ( mzPoly ` V ) )