Theorem dvmptdivc

Description: Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016)

	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)$$
	dvmptcmul.c	$$⊢\phi \to C\in ℂ$$
	dvmptdivc.0	$$⊢\phi \to C\ne 0$$
Assertion	dvmptdivc	$$⊢\phi \to \frac{d\left(x\in X⟼\frac{A}{C}\right)}{d_{S}x}=\left(x\in X⟼\frac{B}{C}\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		dvmptcmul.c	$$⊢\phi \to C\in ℂ$$
6		dvmptdivc.0	$$⊢\phi \to C\ne 0$$
7	5 6	reccld	$$⊢\phi \to \frac{1}{C}\in ℂ$$
8	1 2 3 4 7	dvmptcmul	$$⊢\phi \to \frac{d\left(x\in X⟼\left(\frac{1}{C}\right)A\right)}{d_{S}x}=\left(x\in X⟼\left(\frac{1}{C}\right)B\right)$$
9	5	adantr	$$⊢\left(\phi \wedge x\in X\right)\to C\in ℂ$$
10	6	adantr	$$⊢\left(\phi \wedge x\in X\right)\to C\ne 0$$
11	2 9 10	divrec2d	$$⊢\left(\phi \wedge x\in X\right)\to \frac{A}{C}=\left(\frac{1}{C}\right)A$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in X⟼\frac{A}{C}\right)=\left(x\in X⟼\left(\frac{1}{C}\right)A\right)$$
13	12	oveq2d	$$⊢\phi \to \frac{d\left(x\in X⟼\frac{A}{C}\right)}{d_{S}x}=\frac{d\left(x\in X⟼\left(\frac{1}{C}\right)A\right)}{d_{S}x}$$
14	1 2 3 4	dvmptcl	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$
15	14 9 10	divrec2d	$$⊢\left(\phi \wedge x\in X\right)\to \frac{B}{C}=\left(\frac{1}{C}\right)B$$
16	15	mpteq2dva	$$⊢\phi \to \left(x\in X⟼\frac{B}{C}\right)=\left(x\in X⟼\left(\frac{1}{C}\right)B\right)$$
17	8 13 16	3eqtr4d	$$⊢\phi \to \frac{d\left(x\in X⟼\frac{A}{C}\right)}{d_{S}x}=\left(x\in X⟼\frac{B}{C}\right)$$