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

Proof

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

Metamath Proof Explorer

Theorem rescncf

Proof