mzpnegmpt

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

		Ref	Expression
	Assertion	mzpnegmpt	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ - A) \in mzPoly (V)$

Step	Hyp	Ref	Expression
1		df-neg	$⊢ - A = 0 - A$
2	1	mpteq2i	$⊢ (x \in (ℤ^{V}) ⟼ - A) = (x \in (ℤ^{V}) ⟼ 0 - A)$
3		elfvex	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to V \in V$
4		0z	$⊢ 0 \in ℤ$
5		mzpconstmpt	$⊢ (V \in V \land 0 \in ℤ) \to (x \in (ℤ^{V}) ⟼ 0) \in mzPoly (V)$
6	3 4 5	sylancl	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ 0) \in mzPoly (V)$
7		mzpsubmpt	$⊢ ((x \in (ℤ^{V}) ⟼ 0) \in mzPoly (V) \land (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V)) \to (x \in (ℤ^{V}) ⟼ 0 - A) \in mzPoly (V)$
8	6 7	mpancom	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ 0 - A) \in mzPoly (V)$
9	2 8	eqeltrid	$⊢ (x \in (ℤ^{V}) ⟼ A) \in mzPoly (V) \to (x \in (ℤ^{V}) ⟼ - A) \in mzPoly (V)$

Metamath Proof Explorer