rescncf - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem rescncf 7362

Description: A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.)

**Assertion**
Ref	Expression
rescncf	⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → (F ∈ (A–cn→B) → (F ↾ C) ∈ (C–cn→B)))

**Proof of Theorem rescncf**
Step	Hyp	Ref	Expression
1		fssres 3700	. . . . 5 ⊢ ((F:A–→B ⋀ C ⊆ A) → (F ↾ C):C–→B)
2	1	expcom 381	. . . 4 ⊢ (C ⊆ A → (F:A–→B → (F ↾ C):C–→B))
3		ssralv 2165	. . . . 5 ⊢ (C ⊆ A → (∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y)))
4		ssralv 2165	. . . . . . . . 9 ⊢ (C ⊆ A → (∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y)))
5		fvres 3791	. . . . . . . . . . . . . . 15 ⊢ (x ∈ C → ((F ↾ C) ‘x) = (F ‘x))
6		fvres 3791	. . . . . . . . . . . . . . 15 ⊢ (w ∈ C → ((F ↾ C) ‘w) = (F ‘w))
7	5, 6	opreqan12d 4037	. . . . . . . . . . . . . 14 ⊢ ((x ∈ C ⋀ w ∈ C) → (((F ↾ C) ‘x) − ((F ↾ C) ‘w)) = ((F ‘x) − (F ‘w)))
8	7	fveq2d 3785	. . . . . . . . . . . . 13 ⊢ ((x ∈ C ⋀ w ∈ C) → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) = (abs ‘((F ‘x) − (F ‘w))))
9	8	breq1d 2684	. . . . . . . . . . . 12 ⊢ ((x ∈ C ⋀ w ∈ C) → ((abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y ↔ (abs ‘((F ‘x) − (F ‘w))) < y))
10	9	imbi2d 623	. . . . . . . . . . 11 ⊢ ((x ∈ C ⋀ w ∈ C) → (((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y) ↔ ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y)))
11	10	biimprd 161	. . . . . . . . . 10 ⊢ ((x ∈ C ⋀ w ∈ C) → (((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
12	11	r19.20dva 1756	. . . . . . . . 9 ⊢ (x ∈ C → (∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
13	4, 12	sylan9 479	. . . . . . . 8 ⊢ ((C ⊆ A ⋀ x ∈ C) → (∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
14	13	r19.22sdv 1785	. . . . . . 7 ⊢ ((C ⊆ A ⋀ x ∈ C) → (∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
15	14	r19.20sdv 1757	. . . . . 6 ⊢ ((C ⊆ A ⋀ x ∈ C) → (∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
16	15	r19.20dva 1756	. . . . 5 ⊢ (C ⊆ A → (∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
17	3, 16	syld 27	. . . 4 ⊢ (C ⊆ A → (∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y) → ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y)))
18	2, 17	anim12d 569	. . 3 ⊢ (C ⊆ A → ((F:A–→B ⋀ ∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y)) → ((F ↾ C):C–→B ⋀ ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y))))
19	18	3ad2ant3 814	. 2 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → ((F:A–→B ⋀ ∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y)) → ((F ↾ C):C–→B ⋀ ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y))))
20		elcncf 7355	. . 3 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ) → (F ∈ (A–cn→B) ↔ (F:A–→B ⋀ ∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y))))
21	20	3adant3 811	. 2 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → (F ∈ (A–cn→B) ↔ (F:A–→B ⋀ ∀x ∈ A ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ A ((abs ‘(x − w)) < z → (abs ‘((F ‘x) − (F ‘w))) < y))))
22		sstr 2123	. . . . . 6 ⊢ ((C ⊆ A ⋀ A ⊆ ℂ) → C ⊆ ℂ)
23	22	anim1i 341	. . . . 5 ⊢ (((C ⊆ A ⋀ A ⊆ ℂ) ⋀ B ⊆ ℂ) → (C ⊆ ℂ ⋀ B ⊆ ℂ))
24	23	3impa 840	. . . 4 ⊢ ((C ⊆ A ⋀ A ⊆ ℂ ⋀ B ⊆ ℂ) → (C ⊆ ℂ ⋀ B ⊆ ℂ))
25	24	3coml 852	. . 3 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → (C ⊆ ℂ ⋀ B ⊆ ℂ))
26		elcncf 7355	. . 3 ⊢ ((C ⊆ ℂ ⋀ B ⊆ ℂ) → ((F ↾ C) ∈ (C–cn→B) ↔ ((F ↾ C):C–→B ⋀ ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y))))
27	25, 26	syl 10	. 2 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → ((F ↾ C) ∈ (C–cn→B) ↔ ((F ↾ C):C–→B ⋀ ∀x ∈ C ∀y ∈ ℝ⁺ ∃z ∈ ℝ⁺ ∀w ∈ C ((abs ‘(x − w)) < z → (abs ‘(((F ↾ C) ‘x) − ((F ↾ C) ‘w))) < y))))
28	19, 21, 27	3imtr4d 554	1 ⊢ ((A ⊆ ℂ ⋀ B ⊆ ℂ ⋀ C ⊆ A) → (F ∈ (A–cn→B) → (F ↾ C) ∈ (C–cn→B)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 153 ⋀ wa 230 ⋀ w3a 787 ∈ wcel 999 ∀wral 1692 ∃wrex 1693 ⊆ wss 2098 class class class wbr 2674 ↾ cres 3229 –→wf 3235 ‘cfv 3239 (class class class)co 4021 ℂcc 5297 − cmin 5357 ℝ⁺crp 5365 < clt 5551 abscabs 6840 –cn→ccncf 7352

This theorem is referenced by: isupivthi 7380

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-9 1006 ax-10 1007 ax-11 1008 ax-12 1009 ax-13 1010 ax-14 1011 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 ax-rep 2748 ax-sep 2758 ax-nul 2765 ax-pow 2798 ax-pr 2835 ax-un 2922 ax-inf2 4687

This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-3or 788 df-3an 789 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-ral 1696 df-rex 1697 df-v 1859 df-sbc 1989 df-csb 2052 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-pss 2106 df-nul 2332 df-if 2414 df-pw 2454 df-sn 2464 df-pr 2465 df-tp 2467 df-op 2468 df-uni 2558 df-br 2675 df-opab 2722 df-tr 2736 df-eprel 2888 df-id 2891 df-po 2896 df-so 2906 df-fr 2974 df-we 2991 df-ord 3008 df-on 3009 df-lim 3010 df-suc 3011 df-om 3189 df-xp 3241 df-rel 3242 df-cnv 3243 df-co 3244 df-dm 3245 df-rn 3246 df-res 3247 df-ima 3248 df-fun 3249 df-fn 3250 df-f 3251 df-fv 3255 df-opr 4023 df-oprab 4024 df-qs 4324 df-ni 5065 df-nq 5103 df-np 5151 df-nr 5232 df-c 5305 df-cncf 7353