Metamath Proof Explorer

Theorem rescncf

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)

Ref Expression
Assertion rescncf ⊢C⊆A→F:A⟶cnB→F↾C:C⟶cnB

Proof

Step Hyp Ref Expression
1 simpr ⊢C⊆A∧F:A⟶cnB→F:A⟶cnB
2 cncfrss ⊢F:A⟶cnB→A⊆ℂ
3 2 adantl ⊢C⊆A∧F:A⟶cnB→A⊆ℂ
4 cncfrss2 ⊢F:A⟶cnB→B⊆ℂ
5 4 adantl ⊢C⊆A∧F:A⟶cnB→B⊆ℂ
6 elcncf ⊢A⊆ℂ∧B⊆ℂ→F:A⟶cnB↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y
7 3 5 6 syl2anc ⊢C⊆A∧F:A⟶cnB→F:A⟶cnB↔F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y
8 1 7 mpbid ⊢C⊆A∧F:A⟶cnB→F:A⟶B∧∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y
9 8 simpld ⊢C⊆A∧F:A⟶cnB→F:A⟶B
10 simpl ⊢C⊆A∧F:A⟶cnB→C⊆A
11 9 10 fssresd ⊢C⊆A∧F:A⟶cnB→F↾C:C⟶B
12 8 simprd ⊢C⊆A∧F:A⟶cnB→∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y
13 ssralv ⊢C⊆A→∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y→∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y
14 ssralv ⊢C⊆A→∀w∈Ax−w<z→F⁡x−F⁡w<y→∀w∈Cx−w<z→F⁡x−F⁡w<y
15 fvres ⊢x∈C→F↾C⁡x=F⁡x
16 fvres ⊢w∈C→F↾C⁡w=F⁡w
17 15 16 oveqan12d ⊢x∈C∧w∈C→F↾C⁡x−F↾C⁡w=F⁡x−F⁡w
18 17 fveq2d ⊢x∈C∧w∈C→F↾C⁡x−F↾C⁡w=F⁡x−F⁡w
19 18 breq1d ⊢x∈C∧w∈C→F↾C⁡x−F↾C⁡w<y↔F⁡x−F⁡w<y
20 19 imbi2d ⊢x∈C∧w∈C→x−w<z→F↾C⁡x−F↾C⁡w<y↔x−w<z→F⁡x−F⁡w<y
21 20 biimprd ⊢x∈C∧w∈C→x−w<z→F⁡x−F⁡w<y→x−w<z→F↾C⁡x−F↾C⁡w<y
22 21 ralimdva ⊢x∈C→∀w∈Cx−w<z→F⁡x−F⁡w<y→∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
23 14 22 sylan9 ⊢C⊆A∧x∈C→∀w∈Ax−w<z→F⁡x−F⁡w<y→∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
24 23 reximdv ⊢C⊆A∧x∈C→∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y→∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
25 24 ralimdv ⊢C⊆A∧x∈C→∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y→∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
26 25 ralimdva ⊢C⊆A→∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y→∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
27 13 26 syld ⊢C⊆A→∀x∈A∀y∈ℝ+∃z∈ℝ+∀w∈Ax−w<z→F⁡x−F⁡w<y→∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
28 10 12 27 sylc ⊢C⊆A∧F:A⟶cnB→∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
29 10 3 sstrd ⊢C⊆A∧F:A⟶cnB→C⊆ℂ
30 elcncf ⊢C⊆ℂ∧B⊆ℂ→F↾C:C⟶cnB↔F↾C:C⟶B∧∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
31 29 5 30 syl2anc ⊢C⊆A∧F:A⟶cnB→F↾C:C⟶cnB↔F↾C:C⟶B∧∀x∈C∀y∈ℝ+∃z∈ℝ+∀w∈Cx−w<z→F↾C⁡x−F↾C⁡w<y
32 11 28 31 mpbir2and ⊢C⊆A∧F:A⟶cnB→F↾C:C⟶cnB
33 32 ex ⊢C⊆A→F:A⟶cnB→F↾C:C⟶cnB