Theorem rescncf 25198

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 490	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐹 ∈ (𝐴–cn→𝐵))
2		cncfrss 25192	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
3	2	adantl 487	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐴 ⊆ ℂ)
4		cncfrss2 25193	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
5	4	adantl 487	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐵 ⊆ ℂ)
6		elcncf 25190	. . . . . . 7 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
7	3, 5, 6	syl2anc 596	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
8	1, 7	mpbid 235	. . . . 5 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
9	8	simpld 500	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐹:𝐴⟶𝐵)
10		simpl 488	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐶 ⊆ 𝐴)
11	9, 10	fssresd 6741	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
12	8	simprd 501	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))
13		ssralv 4000	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
14		ssralv 4000	. . . . . . . . 9 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
15		fvres 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
16		fvres 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑤) = (𝐹‘𝑤))
17	15, 16	oveqan12d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤)) = ((𝐹‘𝑥) − (𝐹‘𝑤)))
18	17	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) = (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))))
19	18	breq1d 5113	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → ((abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦 ↔ (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))
20	19	imbi2d 343	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦) ↔ ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
21	20	biimprd 251	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
22	21	ralimdva 3175	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐶 → (∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
23	14, 22	sylan9 517	. . . . . . . 8 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
24	23	reximdv 3178	. . . . . . 7 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
25	24	ralimdv 3177	. . . . . 6 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶) → (∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
26	25	ralimdva 3175	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
27	13, 26	syld 48	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦)))
28	10, 12, 27	sylc 66	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))
29	10, 3	sstrd 3941	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → 𝐶 ⊆ ℂ)
30		elcncf 25190	. . . 4 ⊢ ((𝐶 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → ((𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵) ↔ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))))
31	29, 5, 30	syl2anc 596	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → ((𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵) ↔ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐶 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘(((𝐹 ↾ 𝐶)‘𝑥) − ((𝐹 ↾ 𝐶)‘𝑤))) < 𝑦))))
32	11, 28, 31	mpbir2and 726	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵))
33	32	ex 418	1 ⊢ (𝐶 ⊆ 𝐴 → (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ⊆ wss 3899   class class class wbr 5103   ↾ cres 5653  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412  ℂcc 11179   < clt 11324   − cmin 11522  ℝ⁺crp 13101  abscabs 15381  –cn→ccncf 25177

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833  df-cncf 25179

This theorem is used by:  cpnres  26237  dvlip  26293  dvlip2  26295  c1liplem1  26296  c1lip2  26298  dvgt0lem1  26302  dvivthlem1  26308  dvne0  26311  lhop1lem  26313  dvcnvrelem1  26317  dvcnvrelem2  26318  dvcvx  26320  dvfsumle  26321  dvfsumabs  26323  dvfsumlem2  26327  ftc2ditglem  26345  itgparts  26347  itgsubstlem  26348  itgpowd  26350  psercn2  26732  abelth  26750  abelth2  26751  efcvx  26758  pige3ALT  26830  dvrelog  26947  logcn  26957  logccv  26973  loglesqrt  27071  rpsqrtcn  35205  cxpcncf1  35207  ftc2re  35210  fdvposlt  35211  fdvposle  35213  itgexpif  35218  ftc1cnnclem  38577  ftc2nc  38588  areacirc  38599  cncfres  38667  resopunitintvd  43044  resclunitintvd  43045  lcmineqlem2  43048  aks4d1p1p5  43093  areaquad  44176  lhe4.4ex1a  45272  cncfmptss  46543  resincncf  46829  dvbdfbdioolem1  46882  itgsbtaddcnst  46936  fourierdlem38  47099  fourierdlem46  47106  fourierdlem72  47132  fourierdlem90  47150  fourierdlem111  47171  fouriercn  47186