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

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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptadd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
dvmptadd.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
dvmptadd.dc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
Assertion dvmptmul ( 𝜑 → ( 𝑆 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 dvmulf ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ) = ( ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f + ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) )
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 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 · 𝐶 ) ∈ V )
29 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 · 𝐴 ) ∈ V )
30 23 3 5 4 25 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 · 𝐶 ) ) )
31 23 6 2 7 24 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐷 · 𝐴 ) ) )
32 23 28 29 30 31 offval2 ⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f + ( ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∘f · ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )
33 20 27 32 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )