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

Theorem rescncf 21267
Description: A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.)
Assertion
Ref Expression
rescncf  |-  ( C 
C_  A  ->  ( F  e.  ( A -cn-> B )  ->  ( F  |`  C )  e.  ( C -cn-> B ) ) )

Proof of Theorem rescncf
Dummy variables  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 461 . . . . . 6  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  F  e.  ( A -cn-> B ) )
2 cncfrss 21261 . . . . . . . 8  |-  ( F  e.  ( A -cn-> B )  ->  A  C_  CC )
32adantl 466 . . . . . . 7  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  A  C_  CC )
4 cncfrss2 21262 . . . . . . . 8  |-  ( F  e.  ( A -cn-> B )  ->  B  C_  CC )
54adantl 466 . . . . . . 7  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  B  C_  CC )
6 elcncf 21259 . . . . . . 7  |-  ( ( A  C_  CC  /\  B  C_  CC )  ->  ( F  e.  ( A -cn-> B )  <->  ( F : A --> B  /\  A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) ) ) )
73, 5, 6syl2anc 661 . . . . . 6  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  -> 
( F  e.  ( A -cn-> B )  <->  ( F : A --> B  /\  A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) ) ) )
81, 7mpbid 210 . . . . 5  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  -> 
( F : A --> B  /\  A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) ) )
98simpld 459 . . . 4  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  F : A --> B )
10 simpl 457 . . . 4  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  C  C_  A )
119, 10fssresd 5738 . . 3  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  -> 
( F  |`  C ) : C --> B )
128simprd 463 . . . 4  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) )
13 ssralv 3546 . . . . 5  |-  ( C 
C_  A  ->  ( A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) ) )
14 ssralv 3546 . . . . . . . . 9  |-  ( C 
C_  A  ->  ( A. w  e.  A  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y ) ) )
15 fvres 5866 . . . . . . . . . . . . . . 15  |-  ( x  e.  C  ->  (
( F  |`  C ) `
 x )  =  ( F `  x
) )
16 fvres 5866 . . . . . . . . . . . . . . 15  |-  ( w  e.  C  ->  (
( F  |`  C ) `
 w )  =  ( F `  w
) )
1715, 16oveqan12d 6296 . . . . . . . . . . . . . 14  |-  ( ( x  e.  C  /\  w  e.  C )  ->  ( ( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) )  =  ( ( F `  x )  -  ( F `  w )
) )
1817fveq2d 5856 . . . . . . . . . . . . 13  |-  ( ( x  e.  C  /\  w  e.  C )  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  =  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) ) )
1918breq1d 4443 . . . . . . . . . . . 12  |-  ( ( x  e.  C  /\  w  e.  C )  ->  ( ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y  <->  ( abs `  ( ( F `  x )  -  ( F `  w )
) )  <  y
) )
2019imbi2d 316 . . . . . . . . . . 11  |-  ( ( x  e.  C  /\  w  e.  C )  ->  ( ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y )  <->  ( ( abs `  ( x  -  w ) )  < 
z  ->  ( abs `  ( ( F `  x )  -  ( F `  w )
) )  <  y
) ) )
2120biimprd 223 . . . . . . . . . 10  |-  ( ( x  e.  C  /\  w  e.  C )  ->  ( ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2221ralimdva 2849 . . . . . . . . 9  |-  ( x  e.  C  ->  ( A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2314, 22sylan9 657 . . . . . . . 8  |-  ( ( C  C_  A  /\  x  e.  C )  ->  ( A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2423reximdv 2915 . . . . . . 7  |-  ( ( C  C_  A  /\  x  e.  C )  ->  ( E. z  e.  RR+  A. w  e.  A  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  E. z  e.  RR+  A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2524ralimdv 2851 . . . . . 6  |-  ( ( C  C_  A  /\  x  e.  C )  ->  ( A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  ( x  -  w ) )  < 
z  ->  ( abs `  ( ( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2625ralimdva 2849 . . . . 5  |-  ( C 
C_  A  ->  ( A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2713, 26syld 44 . . . 4  |-  ( C 
C_  A  ->  ( A. x  e.  A  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( F `  x
)  -  ( F `
 w ) ) )  <  y )  ->  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) )
2810, 12, 27sylc 60 . . 3  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) )
2910, 3sstrd 3496 . . . 4  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  ->  C  C_  CC )
30 elcncf 21259 . . . 4  |-  ( ( C  C_  CC  /\  B  C_  CC )  ->  (
( F  |`  C )  e.  ( C -cn-> B )  <->  ( ( F  |`  C ) : C --> B  /\  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  (
x  -  w ) )  <  z  -> 
( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) ) )
3129, 5, 30syl2anc 661 . . 3  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  -> 
( ( F  |`  C )  e.  ( C -cn-> B )  <->  ( ( F  |`  C ) : C --> B  /\  A. x  e.  C  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  C  ( ( abs `  ( x  -  w
) )  <  z  ->  ( abs `  (
( ( F  |`  C ) `  x
)  -  ( ( F  |`  C ) `  w ) ) )  <  y ) ) ) )
3211, 28, 31mpbir2and 920 . 2  |-  ( ( C  C_  A  /\  F  e.  ( A -cn-> B ) )  -> 
( F  |`  C )  e.  ( C -cn-> B ) )
3332ex 434 1  |-  ( C 
C_  A  ->  ( F  e.  ( A -cn-> B )  ->  ( F  |`  C )  e.  ( C -cn-> B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1802   A.wral 2791   E.wrex 2792    C_ wss 3458   class class class wbr 4433    |` cres 4987   -->wf 5570   ` cfv 5574  (class class class)co 6277   CCcc 9488    < clt 9626    - cmin 9805   RR+crp 11224   abscabs 13041   -cn->ccncf 21246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-map 7420  df-cncf 21248
This theorem is referenced by:  cpnres  22206  dvlip  22260  dvlip2  22262  c1liplem1  22263  c1lip2  22265  dvgt0lem1  22269  dvivthlem1  22275  dvne0  22278  lhop1lem  22280  dvcnvrelem1  22284  dvcnvrelem2  22285  dvcvx  22287  dvfsumle  22288  dvfsumabs  22290  dvfsumlem2  22294  ftc2ditglem  22312  itgparts  22314  itgsubstlem  22315  psercn2  22683  abelth  22701  abelth2  22702  efcvx  22709  pige3  22775  dvrelog  22883  logcn  22893  logccv  22909  loglesqrt  22997  ftc1cnnclem  30056  ftc2nc  30067  areacirc  30080  cncfres  30229  itgpowd  31151  areaquad  31153  lhe4.4ex1a  31203  cncfmptss  31505  resincncf  31580  dvbdfbdioolem1  31625  itgsbtaddcnst  31667  fourierdlem38  31812  fourierdlem46  31820  fourierdlem72  31846  fourierdlem90  31864  fourierdlem111  31885  fouriercn  31900
  Copyright terms: Public domain W3C validator