Theorem dvmptdivc

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

	Ref	Expression
Hypotheses	dvmptadd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvmptadd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvmptadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
	dvmptadd.da	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
	dvmptcmul.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	dvmptdivc.0	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	dvmptdivc	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptadd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvmptadd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3		dvmptadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4		dvmptadd.da	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5		dvmptcmul.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6		dvmptdivc.0	⊢ ( 𝜑 → 𝐶 ≠ 0 )
7	5 6	reccld	⊢ ( 𝜑 → ( 1 / 𝐶 ) ∈ ℂ )
8	1 2 3 4 7	dvmptcmul	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 𝐶 ) · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 𝐶 ) · 𝐵 ) ) )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ≠ 0 )
11	2 9 10	divrec2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 / 𝐶 ) = ( ( 1 / 𝐶 ) · 𝐴 ) )
12	11	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 𝐶 ) · 𝐴 ) ) )
13	12	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 𝐶 ) · 𝐴 ) ) ) )
14	1 2 3 4	dvmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
15	14 9 10	divrec2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 / 𝐶 ) = ( ( 1 / 𝐶 ) · 𝐵 ) )
16	15	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 𝐶 ) · 𝐵 ) ) )
17	8 13 16	3eqtr4d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 / 𝐶 ) ) )