Metamath Proof Explorer

Theorem mzpnegmpt

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

Ref Expression
Assertion mzpnegmpt ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ − A ∈ mzPoly ⁡ V

Proof

Step Hyp Ref Expression
1 df-neg ⊢ − A = 0 − A
2 1 mpteq2i ⊢ x ∈ ℤ V ⟼ − A = x ∈ ℤ V ⟼ 0 − A
3 elfvex ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → V ∈ V
4 0z ⊢ 0 ∈ ℤ
5 mzpconstmpt ⊢ V ∈ V ∧ 0 ∈ ℤ → x ∈ ℤ V ⟼ 0 ∈ mzPoly ⁡ V
6 3 4 5 sylancl ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ 0 ∈ mzPoly ⁡ V
7 mzpsubmpt ⊢ x ∈ ℤ V ⟼ 0 ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ 0 − A ∈ mzPoly ⁡ V
8 6 7 mpancom ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ 0 − A ∈ mzPoly ⁡ V
9 2 8 eqeltrid ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ − A ∈ mzPoly ⁡ V