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

Metamath Proof Explorer

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