Metamath Proof Explorer

Theorem mzpsubmpt

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

Ref Expression
Assertion mzpsubmpt ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ B ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A − B ∈ mzPoly ⁡ V

Proof

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