MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvmptco Unicode version

Theorem dvmptco 19317
Description: Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dvmptco  |-  ( ph  ->  ( S  _D  (
x  e.  X  |->  E ) )  =  ( x  e.  X  |->  ( F  x.  B ) ) )
Distinct variable groups:    y, A    x, C    x, D    y, E    y, F    y, T    x, V    x, y, ph    y, W   
x, X    x, Y, y
Allowed substitution groups:    A( x)    B( x, y)    C( y)    D( y)    S( x, y)    T( x)    E( x)    F( x)    V( y)    W( x)    X( y)

Proof of Theorem dvmptco
StepHypRef Expression
1 dvmptco.t . . 3  |-  ( ph  ->  T  e.  { RR ,  CC } )
2 dvmptco.s . . 3  |-  ( ph  ->  S  e.  { RR ,  CC } )
3 dvmptco.c . . . 4  |-  ( (
ph  /\  y  e.  Y )  ->  C  e.  CC )
4 eqid 2286 . . . 4  |-  ( y  e.  Y  |->  C )  =  ( y  e.  Y  |->  C )
53, 4fmptd 5647 . . 3  |-  ( ph  ->  ( y  e.  Y  |->  C ) : Y --> CC )
6 dvmptco.a . . . 4  |-  ( (
ph  /\  x  e.  X )  ->  A  e.  Y )
7 eqid 2286 . . . 4  |-  ( x  e.  X  |->  A )  =  ( x  e.  X  |->  A )
86, 7fmptd 5647 . . 3  |-  ( ph  ->  ( x  e.  X  |->  A ) : X --> Y )
9 dvmptco.dc . . . . 5  |-  ( ph  ->  ( T  _D  (
y  e.  Y  |->  C ) )  =  ( y  e.  Y  |->  D ) )
109dmeqd 4882 . . . 4  |-  ( ph  ->  dom  (  T  _D  ( y  e.  Y  |->  C ) )  =  dom  (  y  e.  Y  |->  D ) )
11 dvmptco.d . . . . . 6  |-  ( (
ph  /\  y  e.  Y )  ->  D  e.  W )
1211ralrimiva 2629 . . . . 5  |-  ( ph  ->  A. y  e.  Y  D  e.  W )
13 dmmptg 5170 . . . . 5  |-  ( A. y  e.  Y  D  e.  W  ->  dom  ( 
y  e.  Y  |->  D )  =  Y )
1412, 13syl 17 . . . 4  |-  ( ph  ->  dom  (  y  e.  Y  |->  D )  =  Y )
1510, 14eqtrd 2318 . . 3  |-  ( ph  ->  dom  (  T  _D  ( y  e.  Y  |->  C ) )  =  Y )
16 dvmptco.da . . . . 5  |-  ( ph  ->  ( S  _D  (
x  e.  X  |->  A ) )  =  ( x  e.  X  |->  B ) )
1716dmeqd 4882 . . . 4  |-  ( ph  ->  dom  (  S  _D  ( x  e.  X  |->  A ) )  =  dom  (  x  e.  X  |->  B ) )
18 dvmptco.b . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  B  e.  V )
1918ralrimiva 2629 . . . . 5  |-  ( ph  ->  A. x  e.  X  B  e.  V )
20 dmmptg 5170 . . . . 5  |-  ( A. x  e.  X  B  e.  V  ->  dom  (  x  e.  X  |->  B )  =  X )
2119, 20syl 17 . . . 4  |-  ( ph  ->  dom  (  x  e.  X  |->  B )  =  X )
2217, 21eqtrd 2318 . . 3  |-  ( ph  ->  dom  (  S  _D  ( x  e.  X  |->  A ) )  =  X )
231, 2, 5, 8, 15, 22dvcof 19293 . 2  |-  ( ph  ->  ( S  _D  (
( y  e.  Y  |->  C )  o.  (
x  e.  X  |->  A ) ) )  =  ( ( ( T  _D  ( y  e.  Y  |->  C ) )  o.  ( x  e.  X  |->  A ) )  o F  x.  ( S  _D  ( x  e.  X  |->  A ) ) ) )
24 eqidd 2287 . . . 4  |-  ( ph  ->  ( x  e.  X  |->  A )  =  ( x  e.  X  |->  A ) )
25 eqidd 2287 . . . 4  |-  ( ph  ->  ( y  e.  Y  |->  C )  =  ( y  e.  Y  |->  C ) )
26 dvmptco.e . . . 4  |-  ( y  =  A  ->  C  =  E )
276, 24, 25, 26fmptco 5654 . . 3  |-  ( ph  ->  ( ( y  e.  Y  |->  C )  o.  ( x  e.  X  |->  A ) )  =  ( x  e.  X  |->  E ) )
2827oveq2d 5837 . 2  |-  ( ph  ->  ( S  _D  (
( y  e.  Y  |->  C )  o.  (
x  e.  X  |->  A ) ) )  =  ( S  _D  (
x  e.  X  |->  E ) ) )
29 ovex 5846 . . . . 5  |-  ( S  _D  ( x  e.  X  |->  A ) )  e.  _V
3029dmex 4942 . . . 4  |-  dom  (  S  _D  ( x  e.  X  |->  A ) )  e.  _V
3122, 30syl6eqelr 2375 . . 3  |-  ( ph  ->  X  e.  _V )
321, 3, 11, 9dvmptcl 19304 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  Y )  ->  D  e.  CC )
33 eqid 2286 . . . . . . . . 9  |-  ( y  e.  Y  |->  D )  =  ( y  e.  Y  |->  D )
3432, 33fmptd 5647 . . . . . . . 8  |-  ( ph  ->  ( y  e.  Y  |->  D ) : Y --> CC )
359feq1d 5346 . . . . . . . 8  |-  ( ph  ->  ( ( T  _D  ( y  e.  Y  |->  C ) ) : Y --> CC  <->  ( y  e.  Y  |->  D ) : Y --> CC ) )
3634, 35mpbird 225 . . . . . . 7  |-  ( ph  ->  ( T  _D  (
y  e.  Y  |->  C ) ) : Y --> CC )
37 fco 5365 . . . . . . 7  |-  ( ( ( 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 )
3836, 8, 37syl2anc 644 . . . . . 6  |-  ( ph  ->  ( ( T  _D  ( y  e.  Y  |->  C ) )  o.  ( x  e.  X  |->  A ) ) : X --> CC )
39 dvmptco.f . . . . . . . 8  |-  ( y  =  A  ->  D  =  F )
406, 24, 9, 39fmptco 5654 . . . . . . 7  |-  ( ph  ->  ( ( T  _D  ( y  e.  Y  |->  C ) )  o.  ( x  e.  X  |->  A ) )  =  ( x  e.  X  |->  F ) )
4140feq1d 5346 . . . . . 6  |-  ( ph  ->  ( ( ( T  _D  ( y  e.  Y  |->  C ) )  o.  ( x  e.  X  |->  A ) ) : X --> CC  <->  ( x  e.  X  |->  F ) : X --> CC ) )
4238, 41mpbid 203 . . . . 5  |-  ( ph  ->  ( x  e.  X  |->  F ) : X --> CC )
43 eqid 2286 . . . . . 6  |-  ( x  e.  X  |->  F )  =  ( x  e.  X  |->  F )
4443fmpt 5644 . . . . 5  |-  ( A. x  e.  X  F  e.  CC  <->  ( x  e.  X  |->  F ) : X --> CC )
4542, 44sylibr 205 . . . 4  |-  ( ph  ->  A. x  e.  X  F  e.  CC )
4645r19.21bi 2644 . . 3  |-  ( (
ph  /\  x  e.  X )  ->  F  e.  CC )
4731, 46, 18, 40, 16offval2 6058 . 2  |-  ( ph  ->  ( ( ( T  _D  ( y  e.  Y  |->  C ) )  o.  ( x  e.  X  |->  A ) )  o F  x.  ( S  _D  ( x  e.  X  |->  A ) ) )  =  ( x  e.  X  |->  ( F  x.  B ) ) )
4823, 28, 473eqtr3d 2326 1  |-  ( ph  ->  ( S  _D  (
x  e.  X  |->  E ) )  =  ( x  e.  X  |->  ( F  x.  B ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1625    e. wcel 1687   A.wral 2546   _Vcvv 2791   {cpr 3644    e. cmpt 4080   dom cdm 4690    o. ccom 4694   -->wf 5219  (class class class)co 5821    o Fcof 6039   CCcc 8732   RRcr 8733    x. cmul 8739    _D cdv 19209
This theorem is referenced by:  dvexp3  19321  dvsincos  19324  dvlipcn  19337  lhop2  19358  itgsubstlem  19391  dvtaylp  19745  taylthlem2  19749  pige3  19881  advlogexp  19998  logtayl  20003  dvcxp1  20078  dvcxp2  20079  loglesqr  20094  dvatan  20227  logdivsum  20678  log2sumbnd  20689  expgrowthi  26951  expgrowth  26953  dvsinexp  27141
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-rep 4134  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-inf2 7339  ax-cnex 8790  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810  ax-pre-mulgt0 8811  ax-pre-sup 8812  ax-addf 8813  ax-mulf 8814
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-reu 2553  df-rmo 2554  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-uni 3831  df-int 3866  df-iun 3910  df-iin 3911  df-br 4027  df-opab 4081  df-mpt 4082  df-tr 4117  df-eprel 4306  df-id 4310  df-po 4315  df-so 4316  df-fr 4353  df-se 4354  df-we 4355  df-ord 4396  df-on 4397  df-lim 4398  df-suc 4399  df-om 4658  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-isom 5232  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-of 6041  df-1st 6085  df-2nd 6086  df-iota 6254  df-riota 6301  df-recs 6385  df-rdg 6420  df-1o 6476  df-2o 6477  df-oadd 6480  df-er 6657  df-map 6771  df-pm 6772  df-ixp 6815  df-en 6861  df-dom 6862  df-sdom 6863  df-fin 6864  df-fi 7162  df-sup 7191  df-oi 7222  df-card 7569  df-cda 7791  df-pnf 8866  df-mnf 8867  df-xr 8868  df-ltxr 8869  df-le 8870  df-sub 9036  df-neg 9037  df-div 9421  df-nn 9744  df-2 9801  df-3 9802  df-4 9803  df-5 9804  df-6 9805  df-7 9806  df-8 9807  df-9 9808  df-10 9809  df-n0 9963  df-z 10022  df-dec 10122  df-uz 10228  df-q 10314  df-rp 10352  df-xneg 10449  df-xadd 10450  df-xmul 10451  df-icc 10659  df-fz 10779  df-fzo 10867  df-seq 11043  df-exp 11101  df-hash 11334  df-cj 11580  df-re 11581  df-im 11582  df-sqr 11716  df-abs 11717  df-struct 13146  df-ndx 13147  df-slot 13148  df-base 13149  df-sets 13150  df-ress 13151  df-plusg 13217  df-mulr 13218  df-starv 13219  df-sca 13220  df-vsca 13221  df-tset 13223  df-ple 13224  df-ds 13226  df-hom 13228  df-cco 13229  df-rest 13323  df-topn 13324  df-topgen 13340  df-pt 13341  df-prds 13344  df-xrs 13399  df-0g 13400  df-gsum 13401  df-qtop 13406  df-imas 13407  df-xps 13409  df-mre 13484  df-mrc 13485  df-acs 13487  df-mnd 14363  df-submnd 14412  df-mulg 14488  df-cntz 14789  df-cmn 15087  df-xmet 16369  df-met 16370  df-bl 16371  df-mopn 16372  df-cnfld 16374  df-top 16632  df-bases 16634  df-topon 16635  df-topsp 16636  df-cld 16752  df-ntr 16753  df-cls 16754  df-nei 16831  df-lp 16864  df-perf 16865  df-cn 16953  df-cnp 16954  df-haus 17039  df-tx 17253  df-hmeo 17442  df-fbas 17516  df-fg 17517  df-fil 17537  df-fm 17629  df-flim 17630  df-flf 17631  df-xms 17881  df-ms 17882  df-tms 17883  df-cncf 18378  df-limc 19212  df-dv 19213
  Copyright terms: Public domain W3C validator