This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion dvmptneg ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ - 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
7 1 2 3 4 6 dvmptcmul ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( - 1 · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( - 1 · 𝐵 ) ) )
8 2 mulm1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( - 1 · 𝐴 ) = - 𝐴 )
9 8 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( - 1 · 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐴 ) )
10 9 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( - 1 · 𝐴 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ - 𝐴 ) ) )
11 1 2 3 4 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
12 11 mulm1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( - 1 · 𝐵 ) = - 𝐵 )
13 12 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( - 1 · 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐵 ) )
14 7 10 13 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ - 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐵 ) )