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 ( 𝑥 ∈ 𝑋 ↦ - 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ - 𝐵 ) )