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 ( 𝑥𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )