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 ⊢Ⅎ_xx∈ℤV⟼A
2 1 nfel1 ⊢Ⅎxx∈ℤV⟼A∈mzPoly⁡V
3 nfmpt1 ⊢Ⅎ_xx∈ℤV⟼B
4 3 nfel1 ⊢Ⅎxx∈ℤV⟼B∈mzPoly⁡V
5 2 4 nfan ⊢Ⅎxx∈ℤ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