Theorem rescncf 24060

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.

Step	Hyp	Ref	Expression
1		simpr 485	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐹 ∈ (𝐴–cn→𝐵))
2		cncfrss 24054	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
3	2	adantl 482	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐴 ⊆ ℂ)
4		cncfrss2 24055	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
5	4	adantl 482	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐵 ⊆ ℂ)
6		elcncf 24052	. . . . . . 7 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
7	3, 5, 6	syl2anc 584	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
8	1, 7	mpbid 231	. . . . 5 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
9	8	simpld 495	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐹:𝐴⟶𝐵)
10		simpl 483	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐶 ⊆ 𝐴)
11	9, 10	fssresd 6641	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
12	8	simprd 496	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))
13		ssralv 3987	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
14		ssralv 3987	. . . . . . . . 9 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
15		fvres 6793	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
16		fvres 6793	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑤) = (𝐹‘𝑤))
17	15, 16	oveqan12d 7294	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤)) = ((𝐹‘𝑥) − (𝐹‘𝑤)))
18	17	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) = (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))))
19	18	breq1d 5084	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → ((abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦 ↔ (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))
20	19	imbi2d 341	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦) ↔ ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
21	20	biimprd 247	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
22	21	ralimdva 3108	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐶 → (∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
23	14, 22	sylan9 508	. . . . . . . 8 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
24	23	reximdv 3202	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
25	24	ralimdv 3109	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
26	25	ralimdva 3108	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
27	13, 26	syld 47	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
28	10, 12, 27	sylc 65	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))
29	10, 3	sstrd 3931	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐶 ⊆ ℂ)
30		elcncf 24052	. . . 4 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → ((𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵) ↔ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))))
31	29, 5, 30	syl2anc 584	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ((𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵) ↔ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))))
32	11, 28, 31	mpbir2and 710	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵))
33	32	ex 413	1 ⊢ (𝐶 ⊆ 𝐴 → (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065   ⊆ wss 3887   class class class wbr 5074   ↾ cres 5591  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  ℂcc 10869   < clt 11009   − cmin 11205  ℝ⁺crp 12730  abscabs 14945  –cn→ccncf 24039

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-map 8617  df-cncf 24041

This theorem is referenced by:  cpnres  25101  dvlip  25157  dvlip2  25159  c1liplem1  25160  c1lip2  25162  dvgt0lem1  25166  dvivthlem1  25172  dvne0  25175  lhop1lem  25177  dvcnvrelem1  25181  dvcnvrelem2  25182  dvcvx  25184  dvfsumle  25185  dvfsumabs  25187  dvfsumlem2  25191  ftc2ditglem  25209  itgparts  25211  itgsubstlem  25212  itgpowd  25214  psercn2  25582  abelth  25600  abelth2  25601  efcvx  25608  pige3ALT  25676  dvrelog  25792  logcn  25802  logccv  25818  loglesqrt  25911  rpsqrtcn  32573  cxpcncf1  32575  ftc2re  32578  fdvposlt  32579  fdvposle  32581  itgexpif  32586  ftc1cnnclem  35848  ftc2nc  35859  areacirc  35870  cncfres  35923  resopunitintvd  40034  resclunitintvd  40035  lcmineqlem2  40038  aks4d1p1p5  40083  areaquad  41047  lhe4.4ex1a  41947  cncfmptss  43128  resincncf  43416  dvbdfbdioolem1  43469  itgsbtaddcnst  43523  fourierdlem38  43686  fourierdlem46  43693  fourierdlem72  43719  fourierdlem90  43737  fourierdlem111  43758  fouriercn  43773