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

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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptadd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
dvmptadd.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
dvmptadd.dc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
Assertion dvmptadd ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 dvmptadd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
6 dvmptadd.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
7 dvmptadd.dc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
8 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
9 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) : 𝑋 ⟶ ℂ )
10 4 dmeqd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
11 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
12 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
13 11 12 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
14 10 13 eqtrd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
15 7 dmeqd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
16 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐷 ∈ 𝑊 )
17 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐷 ∈ 𝑊 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = 𝑋 )
18 16 17 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = 𝑋 )
19 15 18 eqtrd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = 𝑋 )
20 1 8 9 14 19 dvaddf ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f + ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f + ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) )
21 ovex ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ V
22 21 dmex ⊢ dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ V
23 19 22 eqeltrrdi ⊢ ( 𝜑 → 𝑋 ∈ V )
24 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
25 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
26 23 2 5 24 25 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f + ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐶 ) ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f + ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐶 ) ) ) )
28 23 3 6 4 7 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f + ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + 𝐷 ) ) )
29 20 27 28 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + 𝐷 ) ) )