ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvmulxxbr Unicode version

Theorem dvmulxxbr 12709
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12711. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
Hypotheses
Ref Expression
dvadd.f  |-  ( ph  ->  F : X --> CC )
dvadd.x  |-  ( ph  ->  X  C_  S )
dvaddxx.g  |-  ( ph  ->  G : X --> CC )
dvaddbr.s  |-  ( ph  ->  S  C_  CC )
dvadd.bf  |-  ( ph  ->  C ( S  _D  F ) K )
dvadd.bg  |-  ( ph  ->  C ( S  _D  G ) L )
dvaddcntop.j  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
Assertion
Ref Expression
dvmulxxbr  |-  ( ph  ->  C ( S  _D  ( F  oF  x.  G ) ) ( ( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) ) )

Proof of Theorem dvmulxxbr
Dummy variables  y  z  x  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . 4  |-  ( ph  ->  C ( S  _D  F ) K )
2 eqid 2115 . . . . 5  |-  ( Jt  S )  =  ( Jt  S )
3 dvaddcntop.j . . . . 5  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
4 eqid 2115 . . . . 5  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( F `  z )  -  ( F `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( F `  z
)  -  ( F `
 C ) )  /  ( z  -  C ) ) )
5 dvaddbr.s . . . . 5  |-  ( ph  ->  S  C_  CC )
6 dvadd.f . . . . 5  |-  ( ph  ->  F : X --> CC )
7 dvadd.x . . . . 5  |-  ( ph  ->  X  C_  S )
82, 3, 4, 5, 6, 7eldvap 12694 . . . 4  |-  ( ph  ->  ( C ( S  _D  F ) K  <-> 
( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  K  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) ) )
91, 8mpbid 146 . . 3  |-  ( ph  ->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  K  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) )
109simpld 111 . 2  |-  ( ph  ->  C  e.  ( ( int `  ( Jt  S ) ) `  X
) )
117, 5sstrd 3075 . . . . . 6  |-  ( ph  ->  X  C_  CC )
123cntoptopon 12596 . . . . . . . . . 10  |-  J  e.  (TopOn `  CC )
13 resttopon 12235 . . . . . . . . . 10  |-  ( ( J  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  ( Jt  S )  e.  (TopOn `  S ) )
1412, 5, 13sylancr 408 . . . . . . . . 9  |-  ( ph  ->  ( Jt  S )  e.  (TopOn `  S ) )
15 topontop 12076 . . . . . . . . 9  |-  ( ( Jt  S )  e.  (TopOn `  S )  ->  ( Jt  S )  e.  Top )
1614, 15syl 14 . . . . . . . 8  |-  ( ph  ->  ( Jt  S )  e.  Top )
17 toponuni 12077 . . . . . . . . . 10  |-  ( ( Jt  S )  e.  (TopOn `  S )  ->  S  =  U. ( Jt  S ) )
1814, 17syl 14 . . . . . . . . 9  |-  ( ph  ->  S  =  U. ( Jt  S ) )
197, 18sseqtrd 3103 . . . . . . . 8  |-  ( ph  ->  X  C_  U. ( Jt  S ) )
20 eqid 2115 . . . . . . . . 9  |-  U. ( Jt  S )  =  U. ( Jt  S )
2120ntrss2 12185 . . . . . . . 8  |-  ( ( ( Jt  S )  e.  Top  /\  X  C_  U. ( Jt  S ) )  -> 
( ( int `  ( Jt  S ) ) `  X )  C_  X
)
2216, 19, 21syl2anc 406 . . . . . . 7  |-  ( ph  ->  ( ( int `  ( Jt  S ) ) `  X )  C_  X
)
2322, 10sseldd 3066 . . . . . 6  |-  ( ph  ->  C  e.  X )
246, 11, 23dvlemap 12692 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  e.  CC )
25 dvaddxx.g . . . . . . 7  |-  ( ph  ->  G : X --> CC )
2625adantr 272 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  G : X --> CC )
27 elrabi 2808 . . . . . . 7  |-  ( z  e.  { w  e.  X  |  w #  C }  ->  z  e.  X
)
2827adantl 273 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  X )
2926, 28ffvelrnd 5522 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( G `  z
)  e.  CC )
3024, 29mulcld 7750 . . . 4  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  / 
( z  -  C
) )  x.  ( G `  z )
)  e.  CC )
3125, 11, 23dvlemap 12692 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) )  e.  CC )
326, 23ffvelrnd 5522 . . . . . 6  |-  ( ph  ->  ( F `  C
)  e.  CC )
3332adantr 272 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( F `  C
)  e.  CC )
3431, 33mulcld 7750 . . . 4  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
)  e.  CC )
35 ssidd 3086 . . . 4  |-  ( ph  ->  CC  C_  CC )
36 txtopon 12326 . . . . . 6  |-  ( ( J  e.  (TopOn `  CC )  /\  J  e.  (TopOn `  CC )
)  ->  ( J  tX  J )  e.  (TopOn `  ( CC  X.  CC ) ) )
3712, 12, 36mp2an 420 . . . . 5  |-  ( J 
tX  J )  e.  (TopOn `  ( CC  X.  CC ) )
3837toponrestid 12083 . . . 4  |-  ( J 
tX  J )  =  ( ( J  tX  J )t  ( CC  X.  CC ) )
399simprd 113 . . . . 5  |-  ( ph  ->  K  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( F `  z
)  -  ( F `
 C ) )  /  ( z  -  C ) ) ) lim
CC  C ) )
40 cnex 7708 . . . . . . . . . . . . 13  |-  CC  e.  _V
4140a1i 9 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
4241, 5ssexd 4036 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  _V )
43 elpm2r 6526 . . . . . . . . . . . 12  |-  ( ( ( CC  e.  _V  /\  S  e.  _V )  /\  ( G : X --> CC  /\  X  C_  S
) )  ->  G  e.  ( CC  ^pm  S
) )
4441, 42, 25, 7, 43syl22anc 1200 . . . . . . . . . . 11  |-  ( ph  ->  G  e.  ( CC 
^pm  S ) )
45 reldvg 12691 . . . . . . . . . . 11  |-  ( ( S  C_  CC  /\  G  e.  ( CC  ^pm  S
) )  ->  Rel  ( S  _D  G
) )
465, 44, 45syl2anc 406 . . . . . . . . . 10  |-  ( ph  ->  Rel  ( S  _D  G ) )
47 dvadd.bg . . . . . . . . . 10  |-  ( ph  ->  C ( S  _D  G ) L )
48 releldm 4742 . . . . . . . . . 10  |-  ( ( Rel  ( S  _D  G )  /\  C
( S  _D  G
) L )  ->  C  e.  dom  ( S  _D  G ) )
4946, 47, 48syl2anc 406 . . . . . . . . 9  |-  ( ph  ->  C  e.  dom  ( S  _D  G ) )
50 eqid 2115 . . . . . . . . . 10  |-  ( Jt  X )  =  ( Jt  X )
5150, 3dvcnp2cntop 12706 . . . . . . . . 9  |-  ( ( ( S  C_  CC  /\  G : X --> CC  /\  X  C_  S )  /\  C  e.  dom  ( S  _D  G ) )  ->  G  e.  ( ( ( Jt  X )  CnP  J ) `  C ) )
525, 25, 7, 49, 51syl31anc 1202 . . . . . . . 8  |-  ( ph  ->  G  e.  ( ( ( Jt  X )  CnP  J
) `  C )
)
533, 50cnplimccntop 12682 . . . . . . . . 9  |-  ( ( X  C_  CC  /\  C  e.  X )  ->  ( G  e.  ( (
( Jt  X )  CnP  J
) `  C )  <->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C ) ) ) )
5411, 23, 53syl2anc 406 . . . . . . . 8  |-  ( ph  ->  ( G  e.  ( ( ( Jt  X )  CnP  J ) `  C )  <->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C
) ) ) )
5552, 54mpbid 146 . . . . . . 7  |-  ( ph  ->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C ) ) )
5655simprd 113 . . . . . 6  |-  ( ph  ->  ( G `  C
)  e.  ( G lim
CC  C ) )
5725, 11limcdifap 12674 . . . . . . 7  |-  ( ph  ->  ( G lim CC  C
)  =  ( ( G  |`  { w  e.  X  |  w #  C } ) lim CC  C
) )
58 ssrab2 3150 . . . . . . . . . 10  |-  { w  e.  X  |  w #  C }  C_  X
5958a1i 9 . . . . . . . . 9  |-  ( ph  ->  { w  e.  X  |  w #  C }  C_  X )
6025, 59feqresmpt 5441 . . . . . . . 8  |-  ( ph  ->  ( G  |`  { w  e.  X  |  w #  C } )  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) )
6160oveq1d 5755 . . . . . . 7  |-  ( ph  ->  ( ( G  |`  { w  e.  X  |  w #  C }
) lim CC  C )  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `  z ) ) lim CC  C ) )
6257, 61eqtrd 2148 . . . . . 6  |-  ( ph  ->  ( G lim CC  C
)  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) lim
CC  C ) )
6356, 62eleqtrd 2194 . . . . 5  |-  ( ph  ->  ( G `  C
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) lim
CC  C ) )
643mulcncntop 12618 . . . . . 6  |-  x.  e.  ( ( J  tX  J )  Cn  J
)
655, 6, 7dvcl 12695 . . . . . . . 8  |-  ( (
ph  /\  C ( S  _D  F ) K )  ->  K  e.  CC )
661, 65mpdan 415 . . . . . . 7  |-  ( ph  ->  K  e.  CC )
6725, 23ffvelrnd 5522 . . . . . . 7  |-  ( ph  ->  ( G `  C
)  e.  CC )
6866, 67opelxpd 4540 . . . . . 6  |-  ( ph  -> 
<. K ,  ( G `
 C ) >.  e.  ( CC  X.  CC ) )
6937toponunii 12079 . . . . . . 7  |-  ( CC 
X.  CC )  = 
U. ( J  tX  J )
7069cncnpi 12292 . . . . . 6  |-  ( (  x.  e.  ( ( J  tX  J )  Cn  J )  /\  <. K ,  ( G `  C ) >.  e.  ( CC  X.  CC ) )  ->  x.  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. K ,  ( G `  C ) >. )
)
7164, 68, 70sylancr 408 . . . . 5  |-  ( ph  ->  x.  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. K ,  ( G `  C )
>. ) )
7224, 29, 35, 35, 3, 38, 39, 63, 71limccnp2cntop 12689 . . . 4  |-  ( ph  ->  ( K  x.  ( G `  C )
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) ) ) lim
CC  C ) )
73 eqid 2115 . . . . . . . 8  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( G `  z
)  -  ( G `
 C ) )  /  ( z  -  C ) ) )
742, 3, 73, 5, 25, 7eldvap 12694 . . . . . . 7  |-  ( ph  ->  ( C ( S  _D  G ) L  <-> 
( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  L  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) ) )
7547, 74mpbid 146 . . . . . 6  |-  ( ph  ->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  L  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) )
7675simprd 113 . . . . 5  |-  ( ph  ->  L  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( G `  z
)  -  ( G `
 C ) )  /  ( z  -  C ) ) ) lim
CC  C ) )
77 cncfmptc 12646 . . . . . . . 8  |-  ( ( ( F `  C
)  e.  CC  /\  X  C_  CC  /\  CC  C_  CC )  ->  (
z  e.  X  |->  ( F `  C ) )  e.  ( X
-cn-> CC ) )
7832, 11, 35, 77syl3anc 1199 . . . . . . 7  |-  ( ph  ->  ( z  e.  X  |->  ( F `  C
) )  e.  ( X -cn-> CC ) )
79 eqidd 2116 . . . . . . 7  |-  ( z  =  C  ->  ( F `  C )  =  ( F `  C ) )
8078, 23, 79cnmptlimc 12686 . . . . . 6  |-  ( ph  ->  ( F `  C
)  e.  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C ) )
8132adantr 272 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  X )  ->  ( F `  C )  e.  CC )
8281fmpttd 5541 . . . . . . . 8  |-  ( ph  ->  ( z  e.  X  |->  ( F `  C
) ) : X --> CC )
8382, 11limcdifap 12674 . . . . . . 7  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C )  =  ( ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
) lim CC  C )
)
84 resmpt 4835 . . . . . . . . 9  |-  ( { w  e.  X  |  w #  C }  C_  X  ->  ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
)  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) )
8558, 84mp1i 10 . . . . . . . 8  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
)  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) )
8685oveq1d 5755 . . . . . . 7  |-  ( ph  ->  ( ( ( z  e.  X  |->  ( F `
 C ) )  |`  { w  e.  X  |  w #  C }
) lim CC  C )  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) lim CC  C ) )
8783, 86eqtrd 2148 . . . . . 6  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C )  =  ( ( z  e.  {
w  e.  X  |  w #  C }  |->  ( F `
 C ) ) lim
CC  C ) )
8880, 87eleqtrd 2194 . . . . 5  |-  ( ph  ->  ( F `  C
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `
 C ) ) lim
CC  C ) )
895, 25, 7dvcl 12695 . . . . . . . 8  |-  ( (
ph  /\  C ( S  _D  G ) L )  ->  L  e.  CC )
9047, 89mpdan 415 . . . . . . 7  |-  ( ph  ->  L  e.  CC )
9190, 32opelxpd 4540 . . . . . 6  |-  ( ph  -> 
<. L ,  ( F `
 C ) >.  e.  ( CC  X.  CC ) )
9269cncnpi 12292 . . . . . 6  |-  ( (  x.  e.  ( ( J  tX  J )  Cn  J )  /\  <. L ,  ( F `  C ) >.  e.  ( CC  X.  CC ) )  ->  x.  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. L ,  ( F `  C ) >. )
)
9364, 91, 92sylancr 408 . . . . 5  |-  ( ph  ->  x.  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. L ,  ( F `  C )
>. ) )
9431, 33, 35, 35, 3, 38, 76, 88, 93limccnp2cntop 12689 . . . 4  |-  ( ph  ->  ( L  x.  ( F `  C )
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( G `  z )  -  ( G `  C )
)  /  ( z  -  C ) )  x.  ( F `  C ) ) ) lim
CC  C ) )
953addcncntop 12616 . . . . 5  |-  +  e.  ( ( J  tX  J )  Cn  J
)
9666, 67mulcld 7750 . . . . . 6  |-  ( ph  ->  ( K  x.  ( G `  C )
)  e.  CC )
9790, 32mulcld 7750 . . . . . 6  |-  ( ph  ->  ( L  x.  ( F `  C )
)  e.  CC )
9896, 97opelxpd 4540 . . . . 5  |-  ( ph  -> 
<. ( K  x.  ( G `  C )
) ,  ( L  x.  ( F `  C ) ) >.  e.  ( CC  X.  CC ) )
9969cncnpi 12292 . . . . 5  |-  ( (  +  e.  ( ( J  tX  J )  Cn  J )  /\  <.
( K  x.  ( G `  C )
) ,  ( L  x.  ( F `  C ) ) >.  e.  ( CC  X.  CC ) )  ->  +  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. ( K  x.  ( G `
 C ) ) ,  ( L  x.  ( F `  C ) ) >. ) )
10095, 98, 99sylancr 408 . . . 4  |-  ( ph  ->  +  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. ( K  x.  ( G `  C ) ) ,  ( L  x.  ( F `  C ) ) >.
) )
10130, 34, 35, 35, 3, 38, 72, 94, 100limccnp2cntop 12689 . . 3  |-  ( ph  ->  ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) lim CC  C ) )
1026adantr 272 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  F : X --> CC )
103102, 28ffvelrnd 5522 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( F `  z
)  e.  CC )
104103, 33subcld 8037 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  z )  -  ( F `  C )
)  e.  CC )
105104, 29mulcld 7750 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  x.  ( G `
 z ) )  e.  CC )
10667adantr 272 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( G `  C
)  e.  CC )
10729, 106subcld 8037 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( G `  z )  -  ( G `  C )
)  e.  CC )
108107, 33mulcld 7750 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  e.  CC )
10911adantr 272 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  X  C_  CC )
110109, 28sseldd 3066 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  CC )
11111, 23sseldd 3066 . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
112111adantr 272 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  C  e.  CC )
113110, 112subcld 8037 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( z  -  C
)  e.  CC )
114 breq1 3900 . . . . . . . . . . 11  |-  ( w  =  z  ->  (
w #  C  <->  z #  C
) )
115114elrab 2811 . . . . . . . . . 10  |-  ( z  e.  { w  e.  X  |  w #  C } 
<->  ( z  e.  X  /\  z #  C )
)
116115simprbi 271 . . . . . . . . 9  |-  ( z  e.  { w  e.  X  |  w #  C }  ->  z #  C )
117116adantl 273 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z #  C )
118110, 112, 117subap0d 8368 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( z  -  C
) #  0 )
119105, 108, 113, 118divdirapd 8549 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  +  ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) ) )  /  ( z  -  C ) )  =  ( ( ( ( ( F `  z )  -  ( F `  C )
)  x.  ( G `
 z ) )  /  ( z  -  C ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  x.  ( F `  C
) )  /  (
z  -  C ) ) ) )
120103, 29mulcld 7750 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  z )  x.  ( G `  z )
)  e.  CC )
12133, 29mulcld 7750 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  ( G `  z )
)  e.  CC )
12233, 106mulcld 7750 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  ( G `  C )
)  e.  CC )
123120, 121, 122npncand 8061 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  z )
) )  +  ( ( ( F `  C )  x.  ( G `  z )
)  -  ( ( F `  C )  x.  ( G `  C ) ) ) )  =  ( ( ( F `  z
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
124103, 33, 29subdird 8141 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  x.  ( G `
 z ) )  =  ( ( ( F `  z )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  z )
) ) )
125107, 33mulcomd 7751 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  =  ( ( F `
 C )  x.  ( ( G `  z )  -  ( G `  C )
) ) )
12633, 29, 106subdid 8140 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  (
( G `  z
)  -  ( G `
 C ) ) )  =  ( ( ( F `  C
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
127125, 126eqtrd 2148 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  =  ( ( ( F `  C )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  C )
) ) )
128124, 127oveq12d 5758 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  +  ( ( ( G `  z )  -  ( G `  C )
)  x.  ( F `
 C ) ) )  =  ( ( ( ( F `  z )  x.  ( G `  z )
)  -  ( ( F `  C )  x.  ( G `  z ) ) )  +  ( ( ( F `  C )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  C )
) ) ) )
12928, 28elind 3229 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  ( X  i^i  X ) )
1306ffnd 5241 . . . . . . . . . . . 12  |-  ( ph  ->  F  Fn  X )
131130adantr 272 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  F  Fn  X )
13225ffnd 5241 . . . . . . . . . . . 12  |-  ( ph  ->  G  Fn  X )
133132adantr 272 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  G  Fn  X )
134 ssexg 4035 . . . . . . . . . . . . 13  |-  ( ( X  C_  CC  /\  CC  e.  _V )  ->  X  e.  _V )
13511, 40, 134sylancl 407 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  _V )
136135adantr 272 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  X  e.  _V )
137 eqid 2115 . . . . . . . . . . 11  |-  ( X  i^i  X )  =  ( X  i^i  X
)
138 eqidd 2116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  X )  ->  ( F `  z )  =  ( F `  z ) )
139 eqidd 2116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  X )  ->  ( G `  z )  =  ( G `  z ) )
140120adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  ( X  i^i  X ) )  ->  ( ( F `  z )  x.  ( G `  z
) )  e.  CC )
141131, 133, 136, 136, 137, 138, 139, 140ofvalg 5957 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  ( X  i^i  X ) )  ->  ( ( F  oF  x.  G
) `  z )  =  ( ( F `
 z )  x.  ( G `  z
) ) )
142129, 141mpdan 415 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F  oF  x.  G ) `  z )  =  ( ( F `  z
)  x.  ( G `
 z ) ) )
14323, 23elind 3229 . . . . . . . . . 10  |-  ( ph  ->  C  e.  ( X  i^i  X ) )
144 eqidd 2116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  X )  ->  ( F `  C )  =  ( F `  C ) )
145 eqidd 2116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  X )  ->  ( G `  C )  =  ( G `  C ) )
146122adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  ( X  i^i  X ) )  ->  ( ( F `  C )  x.  ( G `  C
) )  e.  CC )
147131, 133, 136, 136, 137, 144, 145, 146ofvalg 5957 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  ( X  i^i  X ) )  ->  ( ( F  oF  x.  G
) `  C )  =  ( ( F `
 C )  x.  ( G `  C
) ) )
148143, 147mpidan 417 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F  oF  x.  G ) `  C )  =  ( ( F `  C
)  x.  ( G `
 C ) ) )
149142, 148oveq12d 5758 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F  oF  x.  G
) `  z )  -  ( ( F  oF  x.  G
) `  C )
)  =  ( ( ( F `  z
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
150123, 128, 1493eqtr4d 2158 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  +  ( ( ( G `  z )  -  ( G `  C )
)  x.  ( F `
 C ) ) )  =  ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) ) )
151150oveq1d 5755 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  +  ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) ) )  /  ( z  -  C ) )  =  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )
152104, 29, 113, 118div23apd 8548 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  /  (
z  -  C ) )  =  ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) ) )
153107, 33, 113, 118div23apd 8548 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( G `  z )  -  ( G `  C ) )  x.  ( F `  C
) )  /  (
z  -  C ) )  =  ( ( ( ( G `  z )  -  ( G `  C )
)  /  ( z  -  C ) )  x.  ( F `  C ) ) )
154152, 153oveq12d 5758 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  / 
( z  -  C
) )  +  ( ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  /  ( z  -  C ) ) )  =  ( ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) )
155119, 151, 1543eqtr3d 2156 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F  oF  x.  G ) `  z
)  -  ( ( F  oF  x.  G ) `  C
) )  /  (
z  -  C ) )  =  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) )
156155mpteq2dva 3986 . . . 4  |-  ( ph  ->  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) )
157156oveq1d 5755 . . 3  |-  ( ph  ->  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z
)  -  ( ( F  oF  x.  G ) `  C
) )  /  (
z  -  C ) ) ) lim CC  C
)  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) lim CC  C ) )
158101, 157eleqtrrd 2195 . 2  |-  ( ph  ->  ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) ) lim CC  C ) )
159 eqid 2115 . . 3  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )
160 mulcl 7711 . . . . 5  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
161160adantl 273 . . . 4  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
162 inidm 3253 . . . 4  |-  ( X  i^i  X )  =  X
163161, 6, 25, 135, 135, 162off 5960 . . 3  |-  ( ph  ->  ( F  oF  x.  G ) : X --> CC )
1642, 3, 159, 5, 163, 7eldvap 12694 . 2  |-  ( ph  ->  ( C ( S  _D  ( F  oF  x.  G )
) ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C )
) )  <->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  (
( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) ) lim CC  C ) ) ) )
16510, 158, 164mpbir2and 911 1  |-  ( ph  ->  C ( S  _D  ( F  oF  x.  G ) ) ( ( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1314    e. wcel 1463   {crab 2395   _Vcvv 2658    i^i cin 3038    C_ wss 3039   <.cop 3498   U.cuni 3704   class class class wbr 3897    |-> cmpt 3957    X. cxp 4505   dom cdm 4507    |` cres 4509    o. ccom 4511   Rel wrel 4512    Fn wfn 5086   -->wf 5087   ` cfv 5091  (class class class)co 5740    oFcof 5946    ^pm cpm 6509   CCcc 7582    + caddc 7587    x. cmul 7589    - cmin 7897   # cap 8306    / cdiv 8392   abscabs 10709   ↾t crest 12015   MetOpencmopn 12049   Topctop 12059  TopOnctopon 12072   intcnt 12157    Cn ccn 12249    CnP ccnp 12250    tX ctx 12316   -cn->ccncf 12621   lim CC climc 12666    _D cdv 12667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704  ax-addf 7706  ax-mulf 7707
This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-of 5948  df-1st 6004  df-2nd 6005  df-recs 6168  df-frec 6254  df-map 6510  df-pm 6511  df-sup 6837  df-inf 6838  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-2 8736  df-3 8737  df-4 8738  df-n0 8929  df-z 9006  df-uz 9276  df-q 9361  df-rp 9391  df-xneg 9499  df-xadd 9500  df-seqfrec 10159  df-exp 10233  df-cj 10554  df-re 10555  df-im 10556  df-rsqrt 10710  df-abs 10711  df-rest 12017  df-topgen 12036  df-psmet 12051  df-xmet 12052  df-met 12053  df-bl 12054  df-mopn 12055  df-top 12060  df-topon 12073  df-bases 12105  df-ntr 12160  df-cn 12252  df-cnp 12253  df-tx 12317  df-cncf 12622  df-limced 12668  df-dvap 12669
This theorem is referenced by:  dvmulxx  12711  dvimulf  12713  dvef  12730
  Copyright terms: Public domain W3C validator