rlimres

Description: The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

		Ref	Expression
	Assertion	rlimres	$⊢ F \underset{ℝ}{⇝} A \to ({F ↾}_{B}) \underset{ℝ}{⇝} A$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ dom F \cap B \subseteq dom F$
2		ssralv	$⊢ dom F \cap B \subseteq dom F \to (\forall z \in dom F (y \leq z \to \|F (z) - A\| < x) \to \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x))$
3	1 2	ax-mp	$⊢ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x) \to \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x)$
4	3	reximi	$⊢ \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x) \to \exists y \in ℝ \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x)$
5	4	ralimi	$⊢ \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x) \to \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x)$
6	5	anim2i	$⊢ (A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x)) \to (A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x))$
7	6	a1i	$⊢ F \underset{ℝ}{⇝} A \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x)) \to (A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x)))$
8		rlimf	$⊢ F \underset{ℝ}{⇝} A \to F : dom F ⟶ ℂ$
9		rlimss	$⊢ F \underset{ℝ}{⇝} A \to dom F \subseteq ℝ$
10		eqidd	$⊢ (F \underset{ℝ}{⇝} A \land z \in dom F) \to F (z) = F (z)$
11	8 9 10	rlim	$⊢ F \underset{ℝ}{⇝} A \to (F \underset{ℝ}{⇝} A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < x)))$
12		fssres	$⊢ (F : dom F ⟶ ℂ \land dom F \cap B \subseteq dom F) \to ({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ ℂ$
13	8 1 12	sylancl	$⊢ F \underset{ℝ}{⇝} A \to ({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ ℂ$
14		resres	$⊢ {({F ↾}_{dom F}) ↾}_{B} = {F ↾}_{(dom F \cap B)}$
15		ffn	$⊢ F : dom F ⟶ ℂ \to F Fn dom F$
16		fnresdm	$⊢ F Fn dom F \to {F ↾}_{dom F} = F$
17	8 15 16	3syl	$⊢ F \underset{ℝ}{⇝} A \to {F ↾}_{dom F} = F$
18	17	reseq1d	$⊢ F \underset{ℝ}{⇝} A \to {({F ↾}_{dom F}) ↾}_{B} = {F ↾}_{B}$
19	14 18	eqtr3id	$⊢ F \underset{ℝ}{⇝} A \to {F ↾}_{(dom F \cap B)} = {F ↾}_{B}$
20	19	feq1d	$⊢ F \underset{ℝ}{⇝} A \to (({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ ℂ \leftrightarrow ({F ↾}_{B}) : dom F \cap B ⟶ ℂ)$
21	13 20	mpbid	$⊢ F \underset{ℝ}{⇝} A \to ({F ↾}_{B}) : dom F \cap B ⟶ ℂ$
22	1 9	sstrid	$⊢ F \underset{ℝ}{⇝} A \to dom F \cap B \subseteq ℝ$
23		elinel2	$⊢ z \in (dom F \cap B) \to z \in B$
24	23	fvresd	$⊢ z \in (dom F \cap B) \to ({F ↾}_{B}) (z) = F (z)$
25	24	adantl	$⊢ (F \underset{ℝ}{⇝} A \land z \in (dom F \cap B)) \to ({F ↾}_{B}) (z) = F (z)$
26	21 22 25	rlim	$⊢ F \underset{ℝ}{⇝} A \to (({F ↾}_{B}) \underset{ℝ}{⇝} A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in (dom F \cap B) (y \leq z \to \|F (z) - A\| < x)))$
27	7 11 26	3imtr4d	$⊢ F \underset{ℝ}{⇝} A \to (F \underset{ℝ}{⇝} A \to ({F ↾}_{B}) \underset{ℝ}{⇝} A)$
28	27	pm2.43i	$⊢ F \underset{ℝ}{⇝} A \to ({F ↾}_{B}) \underset{ℝ}{⇝} A$

Metamath Proof Explorer

Theorem rlimres

Proof