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}\subseteq {A}\to \left({F}:{A}\underset{cn}{⟶}{B}\to \left({{F}↾}_{{C}}\right):{C}\underset{cn}{⟶}{B}\right)$

Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {F}:{A}\underset{cn}{⟶}{B}$
2 cncfrss ${⊢}{F}:{A}\underset{cn}{⟶}{B}\to {A}\subseteq ℂ$
3 2 adantl ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {A}\subseteq ℂ$
4 cncfrss2 ${⊢}{F}:{A}\underset{cn}{⟶}{B}\to {B}\subseteq ℂ$
5 4 adantl ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {B}\subseteq ℂ$
6 elcncf ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to \left({F}:{A}\underset{cn}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)\right)$
7 3 5 6 syl2anc ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({F}:{A}\underset{cn}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)\right)$
8 1 7 mpbid ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)$
9 8 simpld ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {F}:{A}⟶{B}$
10 simpl ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {C}\subseteq {A}$
11 9 10 fssresd ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({{F}↾}_{{C}}\right):{C}⟶{B}$
12 8 simprd ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
13 ssralv ${⊢}{C}\subseteq {A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)$
14 ssralv ${⊢}{C}\subseteq {A}\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)$
15 fvres ${⊢}{x}\in {C}\to \left({{F}↾}_{{C}}\right)\left({x}\right)={F}\left({x}\right)$
16 fvres ${⊢}{w}\in {C}\to \left({{F}↾}_{{C}}\right)\left({w}\right)={F}\left({w}\right)$
17 15 16 oveqan12d ${⊢}\left({x}\in {C}\wedge {w}\in {C}\right)\to \left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)={F}\left({x}\right)-{F}\left({w}\right)$
18 17 fveq2d ${⊢}\left({x}\in {C}\wedge {w}\in {C}\right)\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|=\left|{F}\left({x}\right)-{F}\left({w}\right)\right|$
19 18 breq1d ${⊢}\left({x}\in {C}\wedge {w}\in {C}\right)\to \left(\left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}↔\left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
20 19 imbi2d ${⊢}\left({x}\in {C}\wedge {w}\in {C}\right)\to \left(\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)↔\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)$
21 20 biimprd ${⊢}\left({x}\in {C}\wedge {w}\in {C}\right)\to \left(\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
22 21 ralimdva ${⊢}{x}\in {C}\to \left(\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
23 14 22 sylan9 ${⊢}\left({C}\subseteq {A}\wedge {x}\in {C}\right)\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
24 23 reximdv ${⊢}\left({C}\subseteq {A}\wedge {x}\in {C}\right)\to \left(\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
25 24 ralimdv ${⊢}\left({C}\subseteq {A}\wedge {x}\in {C}\right)\to \left(\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
26 25 ralimdva ${⊢}{C}\subseteq {A}\to \left(\forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
27 13 26 syld ${⊢}{C}\subseteq {A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)$
28 10 12 27 sylc ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)$
29 10 3 sstrd ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {C}\subseteq ℂ$
30 elcncf ${⊢}\left({C}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to \left(\left({{F}↾}_{{C}}\right):{C}\underset{cn}{⟶}{B}↔\left(\left({{F}↾}_{{C}}\right):{C}⟶{B}\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)\right)$
31 29 5 30 syl2anc ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left(\left({{F}↾}_{{C}}\right):{C}\underset{cn}{⟶}{B}↔\left(\left({{F}↾}_{{C}}\right):{C}⟶{B}\wedge \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{w}\right|<{z}\to \left|\left({{F}↾}_{{C}}\right)\left({x}\right)-\left({{F}↾}_{{C}}\right)\left({w}\right)\right|<{y}\right)\right)\right)$
32 11 28 31 mpbir2and ${⊢}\left({C}\subseteq {A}\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{cn}{⟶}{B}$
33 32 ex ${⊢}{C}\subseteq {A}\to \left({F}:{A}\underset{cn}{⟶}{B}\to \left({{F}↾}_{{C}}\right):{C}\underset{cn}{⟶}{B}\right)$