Metamath Proof Explorer

Theorem dvmptco

Description: Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses dvmptco.s 
|- ( ph -> S e. { RR , CC } )
dvmptco.t 
|- ( ph -> T e. { RR , CC } )
dvmptco.a 
|- ( ( ph /\ x e. X ) -> A e. Y )
dvmptco.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptco.c 
|- ( ( ph /\ y e. Y ) -> C e. CC )
dvmptco.d 
|- ( ( ph /\ y e. Y ) -> D e. W )
dvmptco.da 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
dvmptco.dc 
|- ( ph -> ( T _D ( y e. Y |-> C ) ) = ( y e. Y |-> D ) )
dvmptco.e 
|- ( y = A -> C = E )
dvmptco.f 
|- ( y = A -> D = F )
Assertion dvmptco 
|- ( ph -> ( S _D ( x e. X |-> E ) ) = ( x e. X |-> ( F x. B ) ) )

Proof

Step Hyp Ref Expression
1 dvmptco.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptco.t 
 |-  ( ph -> T e. { RR , CC } )
3 dvmptco.a 
 |-  ( ( ph /\ x e. X ) -> A e. Y )
4 dvmptco.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
5 dvmptco.c 
 |-  ( ( ph /\ y e. Y ) -> C e. CC )
6 dvmptco.d 
 |-  ( ( ph /\ y e. Y ) -> D e. W )
7 dvmptco.da 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
8 dvmptco.dc 
 |-  ( ph -> ( T _D ( y e. Y |-> C ) ) = ( y e. Y |-> D ) )
9 dvmptco.e 
 |-  ( y = A -> C = E )
10 dvmptco.f 
 |-  ( y = A -> D = F )
11 5 fmpttd 
 |-  ( ph -> ( y e. Y |-> C ) : Y --> CC )
12 3 fmpttd 
 |-  ( ph -> ( x e. X |-> A ) : X --> Y )
13 8 dmeqd 
 |-  ( ph -> dom ( T _D ( y e. Y |-> C ) ) = dom ( y e. Y |-> D ) )
14 6 ralrimiva 
 |-  ( ph -> A. y e. Y D e. W )
15 dmmptg 
 |-  ( A. y e. Y D e. W -> dom ( y e. Y |-> D ) = Y )
16 14 15 syl 
 |-  ( ph -> dom ( y e. Y |-> D ) = Y )
17 13 16 eqtrd 
 |-  ( ph -> dom ( T _D ( y e. Y |-> C ) ) = Y )
18 7 dmeqd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
19 4 ralrimiva 
 |-  ( ph -> A. x e. X B e. V )
20 dmmptg 
 |-  ( A. x e. X B e. V -> dom ( x e. X |-> B ) = X )
21 19 20 syl 
 |-  ( ph -> dom ( x e. X |-> B ) = X )
22 18 21 eqtrd 
 |-  ( ph -> dom ( S _D ( x e. X |-> A ) ) = X )
23 2 1 11 12 17 22 dvcof 
 |-  ( ph -> ( S _D ( ( y e. Y |-> C ) o. ( x e. X |-> A ) ) ) = ( ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) oF x. ( S _D ( x e. X |-> A ) ) ) )
24 eqidd 
 |-  ( ph -> ( x e. X |-> A ) = ( x e. X |-> A ) )
25 eqidd 
 |-  ( ph -> ( y e. Y |-> C ) = ( y e. Y |-> C ) )
26 3 24 25 9 fmptco 
 |-  ( ph -> ( ( y e. Y |-> C ) o. ( x e. X |-> A ) ) = ( x e. X |-> E ) )
27 26 oveq2d 
 |-  ( ph -> ( S _D ( ( y e. Y |-> C ) o. ( x e. X |-> A ) ) ) = ( S _D ( x e. X |-> E ) ) )
28 ovex 
 |-  ( S _D ( x e. X |-> A ) ) e. _V
29 28 dmex 
 |-  dom ( S _D ( x e. X |-> A ) ) e. _V
30 22 29 eqeltrrdi 
 |-  ( ph -> X e. _V )
31 2 5 6 8 dvmptcl 
 |-  ( ( ph /\ y e. Y ) -> D e. CC )
32 8 31 fmpt3d 
 |-  ( ph -> ( T _D ( y e. Y |-> C ) ) : Y --> CC )
33 fco 
 |-  ( ( ( T _D ( y e. Y |-> C ) ) : Y --> CC /\ ( x e. X |-> A ) : X --> Y ) -> ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) : X --> CC )
34 32 12 33 syl2anc 
 |-  ( ph -> ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) : X --> CC )
35 3 24 8 10 fmptco 
 |-  ( ph -> ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) = ( x e. X |-> F ) )
36 35 feq1d 
 |-  ( ph -> ( ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) : X --> CC <-> ( x e. X |-> F ) : X --> CC ) )
37 34 36 mpbid 
 |-  ( ph -> ( x e. X |-> F ) : X --> CC )
38 37 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> F e. CC )
39 30 38 4 35 7 offval2 
 |-  ( ph -> ( ( ( T _D ( y e. Y |-> C ) ) o. ( x e. X |-> A ) ) oF x. ( S _D ( x e. X |-> A ) ) ) = ( x e. X |-> ( F x. B ) ) )
40 23 27 39 3eqtr3d 
 |-  ( ph -> ( S _D ( x e. X |-> E ) ) = ( x e. X |-> ( F x. B ) ) )