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 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
14 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
15 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
16 5 13 14 15 4syl ⊢ ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
17 6 16 mpbid ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) )
18 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
19 ffun ⊢ ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ → Fun ( 𝑆 D 𝐺 ) )
20 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
21 5 18 19 20 4syl ⊢ ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ↔ 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) ) )
22 7 21 mpbid ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) )
23 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
24 1 2 3 4 12 17 22 23 dvmulbr ⊢ ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) )
25 funbrfv ⊢ ( Fun ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) → ( 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) ) )
26 10 24 25 sylc ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐺 ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) ) )