This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐶 ⊆ 𝐴 → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
2 cncfrss ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ )
3 2 adantl ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐴 ⊆ ℂ )
4 cncfrss2 ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐵 ⊆ ℂ )
5 4 adantl ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐵 ⊆ ℂ )
6 elcncf ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
7 3 5 6 syl2anc ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
8 1 7 mpbid ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
9 8 simpld ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
10 simpl ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐶 ⊆ 𝐴 )
11 9 10 fssresd ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
12 8 simprd ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
13 ssralv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
14 ssralv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
15 fvres ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
16 fvres ⊢ ( 𝑤 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
17 15 16 oveqan12d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) )
18 17 fveq2d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) )
19 18 breq1d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
20 19 imbi2d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
21 20 biimprd ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶 ) → ( ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
22 21 ralimdva ⊢ ( 𝑥 ∈ 𝐶 → ( ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
23 14 22 sylan9 ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
24 23 reximdv ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
25 24 ralimdv ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
26 25 ralimdva ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
27 13 26 syld ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) )
28 10 12 27 sylc ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) )
29 10 3 sstrd ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐶 ⊆ ℂ )
30 elcncf ⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
31 29 5 30 syl2anc ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐶 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) − ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
32 11 28 31 mpbir2and ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) )
33 32 ex ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) )