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	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
Assertion	dvmptneg	$$⊢\phi \to \frac{d\left(x\in X⟼-A\right)}{d_{S}x}=\left(x\in X⟼-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvmptadd.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
3		dvmptadd.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
4		dvmptadd.da	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
5		neg1cn	$$⊢-1\in ℂ$$
6	5	a1i	$$⊢\phi \to -1\in ℂ$$
7	1 2 3 4 6	dvmptcmul	$$⊢\phi \to \frac{d\left(x\in X⟼-1A\right)}{d_{S}x}=\left(x\in X⟼-1B\right)$$
8	2	mulm1d	$$⊢\left(\phi \wedge x\in X\right)\to -1A=-A$$
9	8	mpteq2dva	$$⊢\phi \to \left(x\in X⟼-1A\right)=\left(x\in X⟼-A\right)$$
10	9	oveq2d	$$⊢\phi \to \frac{d\left(x\in X⟼-1A\right)}{d_{S}x}=\frac{d\left(x\in X⟼-A\right)}{d_{S}x}$$
11	1 2 3 4	dvmptcl	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$
12	11	mulm1d	$$⊢\left(\phi \wedge x\in X\right)\to -1B=-B$$
13	12	mpteq2dva	$$⊢\phi \to \left(x\in X⟼-1B\right)=\left(x\in X⟼-B\right)$$
14	7 10 13	3eqtr3d	$$⊢\phi \to \frac{d\left(x\in X⟼-A\right)}{d_{S}x}=\left(x\in X⟼-B\right)$$