Metamath Proof Explorer

Theorem dvcof

Description: The chain rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 10-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvcof.s 
|- ( ph -> S e. { RR , CC } )
dvcof.t 
|- ( ph -> T e. { RR , CC } )
dvcof.f 
|- ( ph -> F : X --> CC )
dvcof.g 
|- ( ph -> G : Y --> X )
dvcof.df 
|- ( ph -> dom ( S _D F ) = X )
dvcof.dg 
|- ( ph -> dom ( T _D G ) = Y )
Assertion dvcof 
|- ( ph -> ( T _D ( F o. G ) ) = ( ( ( S _D F ) o. G ) oF x. ( T _D G ) ) )

Proof

Step Hyp Ref Expression
1 dvcof.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvcof.t 
 |-  ( ph -> T e. { RR , CC } )
3 dvcof.f 
 |-  ( ph -> F : X --> CC )
4 dvcof.g 
 |-  ( ph -> G : Y --> X )
5 dvcof.df 
 |-  ( ph -> dom ( S _D F ) = X )
6 dvcof.dg 
 |-  ( ph -> dom ( T _D G ) = Y )
7 3 adantr 
 |-  ( ( ph /\ x e. Y ) -> F : X --> CC )
8 dvbsss 
 |-  dom ( S _D F ) C_ S
9 5 8 eqsstrrdi 
 |-  ( ph -> X C_ S )
10 9 adantr 
 |-  ( ( ph /\ x e. Y ) -> X C_ S )
11 4 adantr 
 |-  ( ( ph /\ x e. Y ) -> G : Y --> X )
12 dvbsss 
 |-  dom ( T _D G ) C_ T
13 6 12 eqsstrrdi 
 |-  ( ph -> Y C_ T )
14 13 adantr 
 |-  ( ( ph /\ x e. Y ) -> Y C_ T )
15 1 adantr 
 |-  ( ( ph /\ x e. Y ) -> S e. { RR , CC } )
16 2 adantr 
 |-  ( ( ph /\ x e. Y ) -> T e. { RR , CC } )
17 4 ffvelrnda 
 |-  ( ( ph /\ x e. Y ) -> ( G ` x ) e. X )
18 5 adantr 
 |-  ( ( ph /\ x e. Y ) -> dom ( S _D F ) = X )
19 17 18 eleqtrrd 
 |-  ( ( ph /\ x e. Y ) -> ( G ` x ) e. dom ( S _D F ) )
20 6 eleq2d 
 |-  ( ph -> ( x e. dom ( T _D G ) <-> x e. Y ) )
21 20 biimpar 
 |-  ( ( ph /\ x e. Y ) -> x e. dom ( T _D G ) )
22 7 10 11 14 15 16 19 21 dvco 
 |-  ( ( ph /\ x e. Y ) -> ( ( T _D ( F o. G ) ) ` x ) = ( ( ( S _D F ) ` ( G ` x ) ) x. ( ( T _D G ) ` x ) ) )
23 22 mpteq2dva 
 |-  ( ph -> ( x e. Y |-> ( ( T _D ( F o. G ) ) ` x ) ) = ( x e. Y |-> ( ( ( S _D F ) ` ( G ` x ) ) x. ( ( T _D G ) ` x ) ) ) )
24 dvfg 
 |-  ( T e. { RR , CC } -> ( T _D ( F o. G ) ) : dom ( T _D ( F o. G ) ) --> CC )
25 2 24 syl 
 |-  ( ph -> ( T _D ( F o. G ) ) : dom ( T _D ( F o. G ) ) --> CC )
26 recnprss 
 |-  ( T e. { RR , CC } -> T C_ CC )
27 2 26 syl 
 |-  ( ph -> T C_ CC )
28 fco 
 |-  ( ( F : X --> CC /\ G : Y --> X ) -> ( F o. G ) : Y --> CC )
29 3 4 28 syl2anc 
 |-  ( ph -> ( F o. G ) : Y --> CC )
30 27 29 13 dvbss 
 |-  ( ph -> dom ( T _D ( F o. G ) ) C_ Y )
31 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
32 15 31 syl 
 |-  ( ( ph /\ x e. Y ) -> S C_ CC )
33 16 26 syl 
 |-  ( ( ph /\ x e. Y ) -> T C_ CC )
34 fvexd 
 |-  ( ( ph /\ x e. Y ) -> ( ( S _D F ) ` ( G ` x ) ) e. _V )
35 fvexd 
 |-  ( ( ph /\ x e. Y ) -> ( ( T _D G ) ` x ) e. _V )
36 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
37 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
38 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( ( G ` x ) e. dom ( S _D F ) <-> ( G ` x ) ( S _D F ) ( ( S _D F ) ` ( G ` x ) ) ) )
39 15 36 37 38 4syl 
 |-  ( ( ph /\ x e. Y ) -> ( ( G ` x ) e. dom ( S _D F ) <-> ( G ` x ) ( S _D F ) ( ( S _D F ) ` ( G ` x ) ) ) )
40 19 39 mpbid 
 |-  ( ( ph /\ x e. Y ) -> ( G ` x ) ( S _D F ) ( ( S _D F ) ` ( G ` x ) ) )
41 dvfg 
 |-  ( T e. { RR , CC } -> ( T _D G ) : dom ( T _D G ) --> CC )
42 ffun 
 |-  ( ( T _D G ) : dom ( T _D G ) --> CC -> Fun ( T _D G ) )
43 funfvbrb 
 |-  ( Fun ( T _D G ) -> ( x e. dom ( T _D G ) <-> x ( T _D G ) ( ( T _D G ) ` x ) ) )
44 16 41 42 43 4syl 
 |-  ( ( ph /\ x e. Y ) -> ( x e. dom ( T _D G ) <-> x ( T _D G ) ( ( T _D G ) ` x ) ) )
45 21 44 mpbid 
 |-  ( ( ph /\ x e. Y ) -> x ( T _D G ) ( ( T _D G ) ` x ) )
46 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
47 7 10 11 14 32 33 34 35 40 45 46 dvcobr 
 |-  ( ( ph /\ x e. Y ) -> x ( T _D ( F o. G ) ) ( ( ( S _D F ) ` ( G ` x ) ) x. ( ( T _D G ) ` x ) ) )
48 reldv 
 |-  Rel ( T _D ( F o. G ) )
49 48 releldmi 
 |-  ( x ( T _D ( F o. G ) ) ( ( ( S _D F ) ` ( G ` x ) ) x. ( ( T _D G ) ` x ) ) -> x e. dom ( T _D ( F o. G ) ) )
50 47 49 syl 
 |-  ( ( ph /\ x e. Y ) -> x e. dom ( T _D ( F o. G ) ) )
51 30 50 eqelssd 
 |-  ( ph -> dom ( T _D ( F o. G ) ) = Y )
52 51 feq2d 
 |-  ( ph -> ( ( T _D ( F o. G ) ) : dom ( T _D ( F o. G ) ) --> CC <-> ( T _D ( F o. G ) ) : Y --> CC ) )
53 25 52 mpbid 
 |-  ( ph -> ( T _D ( F o. G ) ) : Y --> CC )
54 53 feqmptd 
 |-  ( ph -> ( T _D ( F o. G ) ) = ( x e. Y |-> ( ( T _D ( F o. G ) ) ` x ) ) )
55 2 13 ssexd 
 |-  ( ph -> Y e. _V )
56 4 feqmptd 
 |-  ( ph -> G = ( x e. Y |-> ( G ` x ) ) )
57 1 36 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
58 5 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
59 57 58 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
60 59 feqmptd 
 |-  ( ph -> ( S _D F ) = ( y e. X |-> ( ( S _D F ) ` y ) ) )
61 fveq2 
 |-  ( y = ( G ` x ) -> ( ( S _D F ) ` y ) = ( ( S _D F ) ` ( G ` x ) ) )
62 17 56 60 61 fmptco 
 |-  ( ph -> ( ( S _D F ) o. G ) = ( x e. Y |-> ( ( S _D F ) ` ( G ` x ) ) ) )
63 2 41 syl 
 |-  ( ph -> ( T _D G ) : dom ( T _D G ) --> CC )
64 6 feq2d 
 |-  ( ph -> ( ( T _D G ) : dom ( T _D G ) --> CC <-> ( T _D G ) : Y --> CC ) )
65 63 64 mpbid 
 |-  ( ph -> ( T _D G ) : Y --> CC )
66 65 feqmptd 
 |-  ( ph -> ( T _D G ) = ( x e. Y |-> ( ( T _D G ) ` x ) ) )
67 55 34 35 62 66 offval2 
 |-  ( ph -> ( ( ( S _D F ) o. G ) oF x. ( T _D G ) ) = ( x e. Y |-> ( ( ( S _D F ) ` ( G ` x ) ) x. ( ( T _D G ) ` x ) ) ) )
68 23 54 67 3eqtr4d 
 |-  ( ph -> ( T _D ( F o. G ) ) = ( ( ( S _D F ) o. G ) oF x. ( T _D G ) ) )