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

Theorem rescncf 24283
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 24277 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
32adantl 483 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐴 ⊆ ℂ)
4 cncfrss2 24278 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐵 ⊆ ℂ)
54adantl 483 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐵 ⊆ ℂ)
6 elcncf 24275 . . . . . . 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 6713 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹𝐶):𝐶𝐵)
128simprd 497 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
13 ssralv 4014 . . . . 5 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
14 ssralv 4014 . . . . . . . . 9 (𝐶𝐴 → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
15 fvres 6865 . . . . . . . . . . . . . . 15 (𝑥𝐶 → ((𝐹𝐶)‘𝑥) = (𝐹𝑥))
16 fvres 6865 . . . . . . . . . . . . . . 15 (𝑤𝐶 → ((𝐹𝐶)‘𝑤) = (𝐹𝑤))
1715, 16oveqan12d 7380 . . . . . . . . . . . . . 14 ((𝑥𝐶𝑤𝐶) → (((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤)) = ((𝐹𝑥) − (𝐹𝑤)))
1817fveq2d 6850 . . . . . . . . . . . . 13 ((𝑥𝐶𝑤𝐶) → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) = (abs‘((𝐹𝑥) − (𝐹𝑤))))
1918breq1d 5119 . . . . . . . . . . . 12 ((𝑥𝐶𝑤𝐶) → ((abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦 ↔ (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
2019imbi2d 341 . . . . . . . . . . 11 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦) ↔ ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
2120biimprd 248 . . . . . . . . . 10 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2221ralimdva 3161 . . . . . . . . 9 (𝑥𝐶 → (∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2314, 22sylan9 509 . . . . . . . 8 ((𝐶𝐴𝑥𝐶) → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2423reximdv 3164 . . . . . . 7 ((𝐶𝐴𝑥𝐶) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2524ralimdv 3163 . . . . . 6 ((𝐶𝐴𝑥𝐶) → (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2625ralimdva 3161 . . . . 5 (𝐶𝐴 → (∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2713, 26syld 47 . . . 4 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2810, 12, 27sylc 65 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))
2910, 3sstrd 3958 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐶 ⊆ ℂ)
30 elcncf 24275 . . . 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 3061  wrex 3070  wss 3914   class class class wbr 5109  cres 5639  wf 6496  cfv 6500  (class class class)co 7361  cc 11057   < clt 11197  cmin 11393  +crp 12923  abscabs 15128  cnccncf 24262
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 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115
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 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-map 8773  df-cncf 24264
This theorem is referenced by:  cpnres  25324  dvlip  25380  dvlip2  25382  c1liplem1  25383  c1lip2  25385  dvgt0lem1  25389  dvivthlem1  25395  dvne0  25398  lhop1lem  25400  dvcnvrelem1  25404  dvcnvrelem2  25405  dvcvx  25407  dvfsumle  25408  dvfsumabs  25410  dvfsumlem2  25414  ftc2ditglem  25432  itgparts  25434  itgsubstlem  25435  itgpowd  25437  psercn2  25805  abelth  25823  abelth2  25824  efcvx  25831  pige3ALT  25899  dvrelog  26015  logcn  26025  logccv  26041  loglesqrt  26134  rpsqrtcn  33270  cxpcncf1  33272  ftc2re  33275  fdvposlt  33276  fdvposle  33278  itgexpif  33283  ftc1cnnclem  36199  ftc2nc  36210  areacirc  36221  cncfres  36274  resopunitintvd  40533  resclunitintvd  40534  lcmineqlem2  40537  aks4d1p1p5  40582  areaquad  41597  lhe4.4ex1a  42701  cncfmptss  43918  resincncf  44206  dvbdfbdioolem1  44259  itgsbtaddcnst  44313  fourierdlem38  44476  fourierdlem46  44483  fourierdlem72  44509  fourierdlem90  44527  fourierdlem111  44548  fouriercn  44563
  Copyright terms: Public domain W3C validator