Theorem mzpnegmpt

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

	Ref	Expression
Assertion	mzpnegmpt	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
2	1	mpteq2i	⊢ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 𝐴 ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 0 − 𝐴 ) )
3		elfvex	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
4		0z	⊢ 0 ∈ ℤ
5		mzpconstmpt	⊢ ( ( 𝑉 ∈ V ∧ 0 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 0 ) ∈ ( mzPoly ‘ 𝑉 ) )
6	3 4 5	sylancl	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 0 ) ∈ ( mzPoly ‘ 𝑉 ) )
7		mzpsubmpt	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 0 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 0 − 𝐴 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
8	6 7	mpancom	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 0 − 𝐴 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
9	2 8	eqeltrid	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) )