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→ 𝐵 ) ) )