rlimcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014)

	Ref	Expression
Hypotheses	rlimcn1.1	$⊢ φ \to G : A ⟶ X$
	rlimcn1.2	$⊢ φ \to C \in X$
	rlimcn1.3	$⊢ φ \to G \underset{ℝ}{⇝} C$
	rlimcn1.4	$⊢ φ \to F : X ⟶ ℂ$
	rlimcn1.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x)$
Assertion	rlimcn1	$⊢ φ \to (F \circ G) \underset{ℝ}{⇝} F (C)$

Proof

Step	Hyp	Ref	Expression
1		rlimcn1.1	$⊢ φ \to G : A ⟶ X$
2		rlimcn1.2	$⊢ φ \to C \in X$
3		rlimcn1.3	$⊢ φ \to G \underset{ℝ}{⇝} C$
4		rlimcn1.4	$⊢ φ \to F : X ⟶ ℂ$
5		rlimcn1.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x)$
6	1	ffvelrnda	$⊢ (φ \land w \in A) \to G (w) \in X$
7	1	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
8	4	feqmptd	$⊢ φ \to F = (v \in X ⟼ F (v))$
9		fveq2	$⊢ v = G (w) \to F (v) = F (G (w))$
10	6 7 8 9	fmptco	$⊢ φ \to F \circ G = (w \in A ⟼ F (G (w)))$
11		fvexd	$⊢ (((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \land w \in A) \to G (w) \in V$
12	11	ralrimiva	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to \forall w \in A G (w) \in V$
13		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
14	7 3	eqbrtrrd	$⊢ φ \to (w \in A ⟼ G (w)) \underset{ℝ}{⇝} C$
15	14	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to (w \in A ⟼ G (w)) \underset{ℝ}{⇝} C$
16	12 13 15	rlimi	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|G (w) - C\| < y)$
17		fvoveq1	$⊢ z = G (w) \to \|z - C\| = \|G (w) - C\|$
18	17	breq1d	$⊢ z = G (w) \to (\|z - C\| < y \leftrightarrow \|G (w) - C\| < y)$
19	18	imbrov2fvoveq	$⊢ z = G (w) \to ((\|z - C\| < y \to \|F (z) - F (C)\| < x) \leftrightarrow (\|G (w) - C\| < y \to \|F (G (w)) - F (C)\| < x))$
20		simplrr	$⊢ (((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \land w \in A) \to \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x)$
21	6	ad4ant14	$⊢ (((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \land w \in A) \to G (w) \in X$
22	19 20 21	rspcdva	$⊢ (((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \land w \in A) \to (\|G (w) - C\| < y \to \|F (G (w)) - F (C)\| < x)$
23	22	imim2d	$⊢ (((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \land w \in A) \to ((c \leq w \to \|G (w) - C\| < y) \to (c \leq w \to \|F (G (w)) - F (C)\| < x))$
24	23	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \to (\forall w \in A (c \leq w \to \|G (w) - C\| < y) \to \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x))$
25	24	reximdv	$⊢ ((φ \land x \in ℝ^{+}) \land (y \in ℝ^{+} \land \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x))) \to (\exists c \in ℝ \forall w \in A (c \leq w \to \|G (w) - C\| < y) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x))$
26	25	expr	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to (\forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x) \to (\exists c \in ℝ \forall w \in A (c \leq w \to \|G (w) - C\| < y) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x)))$
27	16 26	mpid	$⊢ ((φ \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to (\forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x))$
28	27	rexlimdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists y \in ℝ^{+} \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x))$
29	5 28	mpd	$⊢ (φ \land x \in ℝ^{+}) \to \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x)$
30	29	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x)$
31	4	ffvelrnda	$⊢ (φ \land G (w) \in X) \to F (G (w)) \in ℂ$
32	6 31	syldan	$⊢ (φ \land w \in A) \to F (G (w)) \in ℂ$
33	32	ralrimiva	$⊢ φ \to \forall w \in A F (G (w)) \in ℂ$
34	1	fdmd	$⊢ φ \to dom G = A$
35		rlimss	$⊢ G \underset{ℝ}{⇝} C \to dom G \subseteq ℝ$
36	3 35	syl	$⊢ φ \to dom G \subseteq ℝ$
37	34 36	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
38	4 2	ffvelrnd	$⊢ φ \to F (C) \in ℂ$
39	33 37 38	rlim2	$⊢ φ \to ((w \in A ⟼ F (G (w))) \underset{ℝ}{⇝} F (C) \leftrightarrow \forall x \in ℝ^{+} \exists c \in ℝ \forall w \in A (c \leq w \to \|F (G (w)) - F (C)\| < x))$
40	30 39	mpbird	$⊢ φ \to (w \in A ⟼ F (G (w))) \underset{ℝ}{⇝} F (C)$
41	10 40	eqbrtrd	$⊢ φ \to (F \circ G) \underset{ℝ}{⇝} F (C)$

Metamath Proof Explorer

Theorem rlimcn1

Proof