Metamath Proof Explorer

Theorem dvmul

Description: The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
dvadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvadd.df ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
dvadd.dg ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
Assertion dvmul ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2 dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
4 dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
5 dvadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
6 dvadd.df ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
7 dvadd.dg ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
8 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ )
9 ffun ⊢ ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) : dom ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ⟶ ℂ → Fun ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
10 5 8 9 3syl ⊢ ( 𝜑 → Fun ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) )
11 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
12 5 11 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
13 fvexd ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ V )
14 fvexd ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ∈ V )
15 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
16 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
17 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
18 5 15 16 17 4syl ⊢ ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
19 6 18 mpbid ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) )
20 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
21 ffun ⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
22 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
23 5 20 21 22 4syl ⊢ ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
24 7 23 mpbid ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) )
25 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
26 1 2 3 4 12 13 14 19 24 25 dvmulbr ⊢ ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) )
27 funbrfv ⊢ ( Fun ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) → ( 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) ) )
28 10 26 27 sylc ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) )