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 
|- ( ph -> F : X --> CC )
dvco.x 
|- ( ph -> X C_ S )
dvco.g 
|- ( ph -> G : Y --> X )
dvco.y 
|- ( ph -> Y C_ T )
dvco.s 
|- ( ph -> S e. { RR , CC } )
dvco.t 
|- ( ph -> T e. { RR , CC } )
dvco.df 
|- ( ph -> ( G ` C ) e. dom ( S _D F ) )
dvco.dg 
|- ( ph -> C e. dom ( T _D G ) )
Assertion dvco 
|- ( ph -> ( ( T _D ( F o. G ) ) ` C ) = ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 dvco.f 
 |-  ( ph -> F : X --> CC )
2 dvco.x 
 |-  ( ph -> X C_ S )
3 dvco.g 
 |-  ( ph -> G : Y --> X )
4 dvco.y 
 |-  ( ph -> Y C_ T )
5 dvco.s 
 |-  ( ph -> S e. { RR , CC } )
6 dvco.t 
 |-  ( ph -> T e. { RR , CC } )
7 dvco.df 
 |-  ( ph -> ( G ` C ) e. dom ( S _D F ) )
8 dvco.dg 
 |-  ( ph -> C e. dom ( T _D G ) )
9 dvfg 
 |-  ( T e. { RR , CC } -> ( T _D ( F o. G ) ) : dom ( T _D ( F o. G ) ) --> CC )
10 ffun 
 |-  ( ( T _D ( F o. G ) ) : dom ( T _D ( F o. G ) ) --> CC -> Fun ( T _D ( F o. G ) ) )
11 6 9 10 3syl 
 |-  ( ph -> Fun ( T _D ( F o. G ) ) )
12 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
13 5 12 syl 
 |-  ( ph -> S C_ CC )
14 recnprss 
 |-  ( T e. { RR , CC } -> T C_ CC )
15 6 14 syl 
 |-  ( ph -> T C_ CC )
16 fvexd 
 |-  ( ph -> ( ( S _D F ) ` ( G ` C ) ) e. _V )
17 fvexd 
 |-  ( ph -> ( ( T _D G ) ` C ) e. _V )
18 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
19 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
20 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( ( G ` C ) e. dom ( S _D F ) <-> ( G ` C ) ( S _D F ) ( ( S _D F ) ` ( G ` C ) ) ) )
21 5 18 19 20 4syl 
 |-  ( ph -> ( ( G ` C ) e. dom ( S _D F ) <-> ( G ` C ) ( S _D F ) ( ( S _D F ) ` ( G ` C ) ) ) )
22 7 21 mpbid 
 |-  ( ph -> ( G ` C ) ( S _D F ) ( ( S _D F ) ` ( G ` C ) ) )
23 dvfg 
 |-  ( T e. { RR , CC } -> ( T _D G ) : dom ( T _D G ) --> CC )
24 ffun 
 |-  ( ( T _D G ) : dom ( T _D G ) --> CC -> Fun ( T _D G ) )
25 funfvbrb 
 |-  ( Fun ( T _D G ) -> ( C e. dom ( T _D G ) <-> C ( T _D G ) ( ( T _D G ) ` C ) ) )
26 6 23 24 25 4syl 
 |-  ( ph -> ( C e. dom ( T _D G ) <-> C ( T _D G ) ( ( T _D G ) ` C ) ) )
27 8 26 mpbid 
 |-  ( ph -> C ( T _D G ) ( ( T _D G ) ` C ) )
28 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
29 1 2 3 4 13 15 16 17 22 27 28 dvcobr 
 |-  ( ph -> C ( T _D ( F o. G ) ) ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) )
30 funbrfv 
 |-  ( Fun ( T _D ( F o. G ) ) -> ( C ( T _D ( F o. G ) ) ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) -> ( ( T _D ( F o. G ) ) ` C ) = ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) ) )
31 11 29 30 sylc 
 |-  ( ph -> ( ( T _D ( F o. G ) ) ` C ) = ( ( ( S _D F ) ` ( G ` C ) ) x. ( ( T _D G ) ` C ) ) )