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

Theorem rescncf 22508
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 476 . . . . . 6 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐹 ∈ (𝐴cn𝐵))
2 cncfrss 22502 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
32adantl 481 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐴 ⊆ ℂ)
4 cncfrss2 22503 . . . . . . . 8 (𝐹 ∈ (𝐴cn𝐵) → 𝐵 ⊆ ℂ)
54adantl 481 . . . . . . 7 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐵 ⊆ ℂ)
6 elcncf 22500 . . . . . . 7 ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
73, 5, 6syl2anc 691 . . . . . 6 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹 ∈ (𝐴cn𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))))
81, 7mpbid 221 . . . . 5 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
98simpld 474 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐹:𝐴𝐵)
10 simpl 472 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐶𝐴)
119, 10fssresd 5984 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹𝐶):𝐶𝐵)
128simprd 478 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
13 ssralv 3629 . . . . 5 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
14 ssralv 3629 . . . . . . . . 9 (𝐶𝐴 → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
15 fvres 6117 . . . . . . . . . . . . . . 15 (𝑥𝐶 → ((𝐹𝐶)‘𝑥) = (𝐹𝑥))
16 fvres 6117 . . . . . . . . . . . . . . 15 (𝑤𝐶 → ((𝐹𝐶)‘𝑤) = (𝐹𝑤))
1715, 16oveqan12d 6568 . . . . . . . . . . . . . 14 ((𝑥𝐶𝑤𝐶) → (((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤)) = ((𝐹𝑥) − (𝐹𝑤)))
1817fveq2d 6107 . . . . . . . . . . . . 13 ((𝑥𝐶𝑤𝐶) → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) = (abs‘((𝐹𝑥) − (𝐹𝑤))))
1918breq1d 4593 . . . . . . . . . . . 12 ((𝑥𝐶𝑤𝐶) → ((abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦 ↔ (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦))
2019imbi2d 329 . . . . . . . . . . 11 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦) ↔ ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦)))
2120biimprd 237 . . . . . . . . . 10 ((𝑥𝐶𝑤𝐶) → (((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2221ralimdva 2945 . . . . . . . . 9 (𝑥𝐶 → (∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2314, 22sylan9 687 . . . . . . . 8 ((𝐶𝐴𝑥𝐶) → (∀𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2423reximdv 2999 . . . . . . 7 ((𝐶𝐴𝑥𝐶) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2524ralimdv 2946 . . . . . 6 ((𝐶𝐴𝑥𝐶) → (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2625ralimdva 2945 . . . . 5 (𝐶𝐴 → (∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2713, 26syld 46 . . . 4 (𝐶𝐴 → (∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘((𝐹𝑥) − (𝐹𝑤))) < 𝑦) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦)))
2810, 12, 27sylc 63 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))
2910, 3sstrd 3578 . . . 4 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → 𝐶 ⊆ ℂ)
30 elcncf 22500 . . . 4 ((𝐶 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → ((𝐹𝐶) ∈ (𝐶cn𝐵) ↔ ((𝐹𝐶):𝐶𝐵 ∧ ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))))
3129, 5, 30syl2anc 691 . . 3 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → ((𝐹𝐶) ∈ (𝐶cn𝐵) ↔ ((𝐹𝐶):𝐶𝐵 ∧ ∀𝑥𝐶𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐶 ((abs‘(𝑥𝑤)) < 𝑧 → (abs‘(((𝐹𝐶)‘𝑥) − ((𝐹𝐶)‘𝑤))) < 𝑦))))
3211, 28, 31mpbir2and 959 . 2 ((𝐶𝐴𝐹 ∈ (𝐴cn𝐵)) → (𝐹𝐶) ∈ (𝐶cn𝐵))
3332ex 449 1 (𝐶𝐴 → (𝐹 ∈ (𝐴cn𝐵) → (𝐹𝐶) ∈ (𝐶cn𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  wcel 1977  wral 2896  wrex 2897  wss 3540   class class class wbr 4583  cres 5040  wf 5800  cfv 5804  (class class class)co 6549  cc 9813   < clt 9953  cmin 10145  +crp 11708  abscabs 13822  cnccncf 22487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-cncf 22489
This theorem is referenced by:  cpnres  23506  dvlip  23560  dvlip2  23562  c1liplem1  23563  c1lip2  23565  dvgt0lem1  23569  dvivthlem1  23575  dvne0  23578  lhop1lem  23580  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcvx  23587  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  ftc2ditglem  23612  itgparts  23614  itgsubstlem  23615  psercn2  23981  abelth  23999  abelth2  24000  efcvx  24007  pige3  24073  dvrelog  24183  logcn  24193  logccv  24209  loglesqrt  24299  ftc1cnnclem  32653  ftc2nc  32664  areacirc  32675  cncfres  32734  itgpowd  36819  areaquad  36821  lhe4.4ex1a  37550  cncfmptss  38654  resincncf  38760  dvbdfbdioolem1  38818  itgsbtaddcnst  38874  fourierdlem38  39038  fourierdlem46  39045  fourierdlem72  39071  fourierdlem90  39089  fourierdlem111  39110  fouriercn  39125
  Copyright terms: Public domain W3C validator