Metamath Proof Explorer

Theorem dvmptadd

Description: Function-builder for derivative, addition 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 dvmptadd ⊢ φ → dx ∈ X A + C dS x = x ∈ X ⟼ B + D

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 dvaddf ⊢ φ → S D x ∈ X ⟼ A + f x ∈ X ⟼ C = dx ∈ X A dS x + f dx ∈ X C dS x
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 23 3 6 4 7 offval2 ⊢ φ → dx ∈ X A dS x + f dx ∈ X C dS x = x ∈ X ⟼ B + D
29 20 27 28 3eqtr3d ⊢ φ → dx ∈ X A + C dS x = x ∈ X ⟼ B + D