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

Metamath Proof Explorer

Theorem dvco

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

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

Proof

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