Theorem mzpsubmpt

Description: The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	mzpsubmpt	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 − 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 )
2	1	nfel1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 )
3		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 )
4	3	nfel1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 )
5	2 4	nfan	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) )
6		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
7	6	ad2antlr	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
8		simpr	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝑥 ∈ ( ℤ ↑m 𝑉 ) )
9		mptfcl	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) → 𝐵 ∈ ℤ ) )
10	7 8 9	sylc	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐵 ∈ ℤ )
11	10	zcnd	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐵 ∈ ℂ )
12	11	mulm1d	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( - 1 · 𝐵 ) = - 𝐵 )
13	12	oveq2d	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 + - 𝐵 ) )
14		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
15	14	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
16		mptfcl	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) → 𝐴 ∈ ℤ ) )
17	15 8 16	sylc	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐴 ∈ ℤ )
18	17	zcnd	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → 𝐴 ∈ ℂ )
19	18 11	negsubd	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
20	13 19	eqtr2d	⊢ ( ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ℤ ↑m 𝑉 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
21	5 20	mpteq2da	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 − 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + ( - 1 · 𝐵 ) ) ) )
22		elfvex	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → 𝑉 ∈ V )
23		neg1z	⊢ - 1 ∈ ℤ
24		mzpconstmpt	⊢ ( ( 𝑉 ∈ V ∧ - 1 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 1 ) ∈ ( mzPoly ‘ 𝑉 ) )
25	22 23 24	sylancl	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 1 ) ∈ ( mzPoly ‘ 𝑉 ) )
26		mzpmulmpt	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ - 1 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( - 1 · 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
27	25 26	mpancom	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( - 1 · 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
28		mzpaddmpt	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( - 1 · 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) )
29	27 28	sylan2	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + ( - 1 · 𝐵 ) ) ) ∈ ( mzPoly ‘ 𝑉 ) )
30	21 29	eqeltrd	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 − 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )