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

Theorem rescncf 24413
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 (𝐶𝐴 → (𝐹 ∈ (𝐴cn𝐵) → (𝐹𝐶) ∈ (𝐶cn𝐵)))

Proof of Theorem rescncf
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 486 . . . . . 6 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐹 ∈ (𝐴cn𝐵))
2 cncfrss 24407 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
32adantl 483 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐴 ⊆ ℂ)
4 cncfrss2 24408 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐵 ⊆ ℂ)
54adantl 483 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐵 ⊆ ℂ)
6 elcncf 24405 . . . . . . 7 ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
73, 5, 6syl2anc 585 . . . . . 6 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
81, 7mpbid 231 . . . . 5 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
98simpld 496 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐹:𝐴𝐵)
10 simpl 484 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐶𝐴)
119, 10fssresd 6759 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹𝐶):𝐶𝐵)
128simprd 497 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
13 ssralv 4051 . . . . 5 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
14 ssralv 4051 . . . . . . . . 9 (𝐶𝐴 → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
15 fvres 6911 . . . . . . . . . . . . . . 15 (𝑥𝐶 → ((𝐹𝐶)‘𝑥) = (𝐹𝑥))
16 fvres 6911 . . . . . . . . . . . . . . 15 (𝑤𝐶 → ((𝐹𝐶)‘𝑤) = (𝐹𝑤))
1715, 16oveqan12d 7428 . . . . . . . . . . . . . 14 ((𝑥𝐶𝑤𝐶) → (((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤)) = ((𝐹𝑥) − (𝐹𝑤)))
1817fveq2d 6896 . . . . . . . . . . . . 13 ((𝑥𝐶𝑤𝐶) → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) = (abs‘((𝐹𝑥) − (𝐹𝑤))))
1918breq1d 5159 . . . . . . . . . . . 12 ((𝑥𝐶𝑤𝐶) → ((abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦 ↔ (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
2019imbi2d 341 . . . . . . . . . . 11 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦) ↔ ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
2120biimprd 247 . . . . . . . . . 10 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2221ralimdva 3168 . . . . . . . . 9 (𝑥𝐶 → (∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2314, 22sylan9 509 . . . . . . . 8 ((𝐶𝐴𝑥𝐶) → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2423reximdv 3171 . . . . . . 7 ((𝐶𝐴𝑥𝐶) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2524ralimdv 3170 . . . . . 6 ((𝐶𝐴𝑥𝐶) → (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2625ralimdva 3168 . . . . 5 (𝐶𝐴 → (∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2713, 26syld 47 . . . 4 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2810, 12, 27sylc 65 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))
2910, 3sstrd 3993 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐶 ⊆ ℂ)
30 elcncf 24405 . . . 4 ((𝐶 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → ((𝐹𝐶) ∈ (𝐶cn𝐵) ↔ ((𝐹𝐶):𝐶𝐵 ∧ ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))))
3129, 5, 30syl2anc 585 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ((𝐹𝐶) ∈ (𝐶cn𝐵) ↔ ((𝐹𝐶):𝐶𝐵 ∧ ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))))
3211, 28, 31mpbir2and 712 . 2 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹𝐶) ∈ (𝐶cn𝐵))
3332ex 414 1 (𝐶𝐴 → (𝐹 ∈ (𝐴cn𝐵) → (𝐹𝐶) ∈ (𝐶cn𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wral 3062  wrex 3071  wss 3949   class class class wbr 5149  cres 5679  wf 6540  cfv 6544  (class class class)co 7409  cc 11108   < clt 11248  cmin 11444  +crp 12974  abscabs 15181  cnccncf 24392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-map 8822  df-cncf 24394
This theorem is referenced by:  cpnres  25454  dvlip  25510  dvlip2  25512  c1liplem1  25513  c1lip2  25515  dvgt0lem1  25519  dvivthlem1  25525  dvne0  25528  lhop1lem  25530  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcvx  25537  dvfsumle  25538  dvfsumabs  25540  dvfsumlem2  25544  ftc2ditglem  25562  itgparts  25564  itgsubstlem  25565  itgpowd  25567  psercn2  25935  abelth  25953  abelth2  25954  efcvx  25961  pige3ALT  26029  dvrelog  26145  logcn  26155  logccv  26171  loglesqrt  26266  rpsqrtcn  33605  cxpcncf1  33607  ftc2re  33610  fdvposlt  33611  fdvposle  33613  itgexpif  33618  gg-psercn2  35178  gg-dvfsumle  35182  gg-dvfsumlem2  35183  ftc1cnnclem  36559  ftc2nc  36570  areacirc  36581  cncfres  36633  resopunitintvd  40891  resclunitintvd  40892  lcmineqlem2  40895  aks4d1p1p5  40940  areaquad  41965  lhe4.4ex1a  43088  cncfmptss  44303  resincncf  44591  dvbdfbdioolem1  44644  itgsbtaddcnst  44698  fourierdlem38  44861  fourierdlem46  44868  fourierdlem72  44894  fourierdlem90  44912  fourierdlem111  44933  fouriercn  44948
  Copyright terms: Public domain W3C validator