Metamath Proof Explorer

Theorem dvmptneg

Description: Function-builder for derivative, product rule for negatives. (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
Assertion dvmptneg ⊢ φ → dx ∈ X − A dS x = x ∈ X ⟼ − B

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 neg1cn ⊢ − 1 ∈ ℂ
6 5 a1i ⊢ φ → − 1 ∈ ℂ
7 1 2 3 4 6 dvmptcmul ⊢ φ → dx ∈ X -1 ⁢ A dS x = x ∈ X ⟼ -1 ⁢ B
8 2 mulm1d ⊢ φ ∧ x ∈ X → -1 ⁢ A = − A
9 8 mpteq2dva ⊢ φ → x ∈ X ⟼ -1 ⁢ A = x ∈ X ⟼ − A
10 9 oveq2d ⊢ φ → dx ∈ X -1 ⁢ A dS x = dx ∈ X − A dS x
11 1 2 3 4 dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ
12 11 mulm1d ⊢ φ ∧ x ∈ X → -1 ⁢ B = − B
13 12 mpteq2dva ⊢ φ → x ∈ X ⟼ -1 ⁢ B = x ∈ X ⟼ − B
14 7 10 13 3eqtr3d ⊢ φ → dx ∈ X − A dS x = x ∈ X ⟼ − B