Metamath Proof Explorer

Theorem dvmptsub

Description: Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s ⊢ φ → S ∈ ℝ ℂ
dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
dvmptsub.c ⊢ φ ∧ x ∈ X → C ∈ ℂ
dvmptsub.d ⊢ φ ∧ x ∈ X → D ∈ W
dvmptsub.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
Assertion dvmptsub ⊢ φ → dx ∈ X A − C dS x = x ∈ X ⟼ B − D

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ φ → S ∈ ℝ ℂ
2 dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
3 dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
4 dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
5 dvmptsub.c ⊢ φ ∧ x ∈ X → C ∈ ℂ
6 dvmptsub.d ⊢ φ ∧ x ∈ X → D ∈ W
7 dvmptsub.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
8 5 negcld ⊢ φ ∧ x ∈ X → − C ∈ ℂ
9 negex ⊢ − D ∈ V
10 9 a1i ⊢ φ ∧ x ∈ X → − D ∈ V
11 1 5 6 7 dvmptneg ⊢ φ → dx ∈ X − C dS x = x ∈ X ⟼ − D
12 1 2 3 4 8 10 11 dvmptadd ⊢ φ → dx ∈ X A + − C dS x = x ∈ X ⟼ B + − D
13 2 5 negsubd ⊢ φ ∧ x ∈ X → A + − C = A − C
14 13 mpteq2dva ⊢ φ → x ∈ X ⟼ A + − C = x ∈ X ⟼ A − C
15 14 oveq2d ⊢ φ → dx ∈ X A + − C dS x = dx ∈ X A − C dS x
16 1 2 3 4 dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ
17 1 5 6 7 dvmptcl ⊢ φ ∧ x ∈ X → D ∈ ℂ
18 16 17 negsubd ⊢ φ ∧ x ∈ X → B + − D = B − D
19 18 mpteq2dva ⊢ φ → x ∈ X ⟼ B + − D = x ∈ X ⟼ B − D
20 12 15 19 3eqtr3d ⊢ φ → dx ∈ X A − C dS x = x ∈ X ⟼ B − D