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 ⊢ φ → S ∈ ℝ ℂ
dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
dvmptcmul.c ⊢ φ → C ∈ ℂ
dvmptdivc.0 ⊢ φ → C ≠ 0
Assertion dvmptdivc ⊢ φ → dx ∈ X A C dS x = x ∈ X ⟼ B C

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ φ → S ∈ ℝ ℂ
2 dvmptadd.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
3 dvmptadd.b ⊢ φ ∧ x ∈ X → B ∈ V
4 dvmptadd.da ⊢ φ → dx ∈ X A dS x = x ∈ X ⟼ B
5 dvmptcmul.c ⊢ φ → C ∈ ℂ
6 dvmptdivc.0 ⊢ φ → C ≠ 0
7 5 6 reccld ⊢ φ → 1 C ∈ ℂ
8 1 2 3 4 7 dvmptcmul ⊢ φ → dx ∈ X 1 C ⁢ A dS x = x ∈ X ⟼ 1 C ⁢ B
9 5 adantr ⊢ φ ∧ x ∈ X → C ∈ ℂ
10 6 adantr ⊢ φ ∧ x ∈ X → C ≠ 0
11 2 9 10 divrec2d ⊢ φ ∧ x ∈ X → A C = 1 C ⁢ A
12 11 mpteq2dva ⊢ φ → x ∈ X ⟼ A C = x ∈ X ⟼ 1 C ⁢ A
13 12 oveq2d ⊢ φ → dx ∈ X A C dS x = dx ∈ X 1 C ⁢ A dS x
14 1 2 3 4 dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ
15 14 9 10 divrec2d ⊢ φ ∧ x ∈ X → B C = 1 C ⁢ B
16 15 mpteq2dva ⊢ φ → x ∈ X ⟼ B C = x ∈ X ⟼ 1 C ⁢ B
17 8 13 16 3eqtr4d ⊢ φ → dx ∈ X A C dS x = x ∈ X ⟼ B C