Metamath Proof Explorer

Theorem dvmptmul

Description: Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

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
dvmptadd.c ⊢ φ ∧ x ∈ X → C ∈ ℂ
dvmptadd.d ⊢ φ ∧ x ∈ X → D ∈ W
dvmptadd.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
Assertion dvmptmul ⊢ φ → dx ∈ X A ⁢ C dS x = x ∈ X ⟼ B ⁢ C + D ⁢ A

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 dvmptadd.c ⊢ φ ∧ x ∈ X → C ∈ ℂ
6 dvmptadd.d ⊢ φ ∧ x ∈ X → D ∈ W
7 dvmptadd.dc ⊢ φ → dx ∈ X C dS x = x ∈ X ⟼ D
8 2 fmpttd ⊢ φ → x ∈ X ⟼ A : X ⟶ ℂ
9 5 fmpttd ⊢ φ → x ∈ X ⟼ C : X ⟶ ℂ
10 4 dmeqd ⊢ φ → dom ⁡ dx ∈ X A dS x = dom ⁡ x ∈ X ⟼ B
11 3 ralrimiva ⊢ φ → ∀ x ∈ X B ∈ V
12 dmmptg ⊢ ∀ x ∈ X B ∈ V → dom ⁡ x ∈ X ⟼ B = X
13 11 12 syl ⊢ φ → dom ⁡ x ∈ X ⟼ B = X
14 10 13 eqtrd ⊢ φ → dom ⁡ dx ∈ X A dS x = X
15 7 dmeqd ⊢ φ → dom ⁡ dx ∈ X C dS x = dom ⁡ x ∈ X ⟼ D
16 6 ralrimiva ⊢ φ → ∀ x ∈ X D ∈ W
17 dmmptg ⊢ ∀ x ∈ X D ∈ W → dom ⁡ x ∈ X ⟼ D = X
18 16 17 syl ⊢ φ → dom ⁡ x ∈ X ⟼ D = X
19 15 18 eqtrd ⊢ φ → dom ⁡ dx ∈ X C dS x = X
20 1 8 9 14 19 dvmulf ⊢ φ → S D x ∈ X ⟼ A × f x ∈ X ⟼ C = dx ∈ X A dS x × f x ∈ X ⟼ C + f dx ∈ X C dS x × f x ∈ X ⟼ A
21 ovex ⊢ dx ∈ X C dS x ∈ V
22 21 dmex ⊢ dom ⁡ dx ∈ X C dS x ∈ V
23 19 22 eqeltrrdi ⊢ φ → X ∈ V
24 eqidd ⊢ φ → x ∈ X ⟼ A = x ∈ X ⟼ A
25 eqidd ⊢ φ → x ∈ X ⟼ C = x ∈ X ⟼ C
26 23 2 5 24 25 offval2 ⊢ φ → x ∈ X ⟼ A × f x ∈ X ⟼ C = x ∈ X ⟼ A ⁢ C
27 26 oveq2d ⊢ φ → S D x ∈ X ⟼ A × f x ∈ X ⟼ C = dx ∈ X A ⁢ C dS x
28 ovexd ⊢ φ ∧ x ∈ X → B ⁢ C ∈ V
29 ovexd ⊢ φ ∧ x ∈ X → D ⁢ A ∈ V
30 23 3 5 4 25 offval2 ⊢ φ → dx ∈ X A dS x × f x ∈ X ⟼ C = x ∈ X ⟼ B ⁢ C
31 23 6 2 7 24 offval2 ⊢ φ → dx ∈ X C dS x × f x ∈ X ⟼ A = x ∈ X ⟼ D ⁢ A
32 23 28 29 30 31 offval2 ⊢ φ → dx ∈ X A dS x × f x ∈ X ⟼ C + f dx ∈ X C dS x × f x ∈ X ⟼ A = x ∈ X ⟼ B ⁢ C + D ⁢ A
33 20 27 32 3eqtr3d ⊢ φ → dx ∈ X A ⁢ C dS x = x ∈ X ⟼ B ⁢ C + D ⁢ A