Theorem mzpnegmpt

Description: Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Assertion	mzpnegmpt	|- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u A ) e. ( mzPoly ` V ) )

Proof

Step	Hyp	Ref	Expression
1		df-neg	|- -u A = ( 0 - A )
2	1	mpteq2i	|- ( x e. ( ZZ ^m V ) |-> -u A ) = ( x e. ( ZZ ^m V ) |-> ( 0 - A ) )
3		elfvex	|- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> V e. _V )
4		0z	|- 0 e. ZZ
5		mzpconstmpt	|- ( ( V e. _V /\ 0 e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> 0 ) e. ( mzPoly ` V ) )
6	3 4 5	sylancl	|- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> 0 ) e. ( mzPoly ` V ) )
7		mzpsubmpt	|- ( ( ( x e. ( ZZ ^m V ) |-> 0 ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( 0 - A ) ) e. ( mzPoly ` V ) )
8	6 7	mpancom	|- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( 0 - A ) ) e. ( mzPoly ` V ) )
9	2 8	eqeltrid	|- ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u A ) e. ( mzPoly ` V ) )