rlimcn2

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

	Ref	Expression
Hypotheses	rlimcn2.1a	$⊢ (φ \land z \in A) \to B \in X$
	rlimcn2.1b	$⊢ (φ \land z \in A) \to C \in Y$
	rlimcn2.2a	$⊢ φ \to R \in X$
	rlimcn2.2b	$⊢ φ \to S \in Y$
	rlimcn2.3a	$⊢ φ \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
	rlimcn2.3b	$⊢ φ \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
	rlimcn2.4	$⊢ φ \to F : X \times Y ⟶ ℂ$
	rlimcn2.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)$
Assertion	rlimcn2	$⊢ φ \to (z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S)$

Proof

Step	Hyp	Ref	Expression
1		rlimcn2.1a	$⊢ (φ \land z \in A) \to B \in X$
2		rlimcn2.1b	$⊢ (φ \land z \in A) \to C \in Y$
3		rlimcn2.2a	$⊢ φ \to R \in X$
4		rlimcn2.2b	$⊢ φ \to S \in Y$
5		rlimcn2.3a	$⊢ φ \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
6		rlimcn2.3b	$⊢ φ \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
7		rlimcn2.4	$⊢ φ \to F : X \times Y ⟶ ℂ$
8		rlimcn2.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)$
9	1	ralrimiva	$⊢ φ \to \forall z \in A B \in X$
10	9	adantr	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to \forall z \in A B \in X$
11		simprl	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to r \in ℝ^{+}$
12	5	adantr	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
13	10 11 12	rlimi	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to \exists a \in ℝ \forall z \in A (a \leq z \to \|B - R\| < r)$
14	2	ralrimiva	$⊢ φ \to \forall z \in A C \in Y$
15	14	adantr	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to \forall z \in A C \in Y$
16		simprr	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to s \in ℝ^{+}$
17	6	adantr	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
18	15 16 17	rlimi	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to \exists b \in ℝ \forall z \in A (b \leq z \to \|C - S\| < s)$
19		reeanv	$⊢ \exists a \in ℝ \exists b \in ℝ (\forall z \in A (a \leq z \to \|B - R\| < r) \land \forall z \in A (b \leq z \to \|C - S\| < s)) \leftrightarrow (\exists a \in ℝ \forall z \in A (a \leq z \to \|B - R\| < r) \land \exists b \in ℝ \forall z \in A (b \leq z \to \|C - S\| < s))$
20		r19.26	$⊢ \forall z \in A ((a \leq z \to \|B - R\| < r) \land (b \leq z \to \|C - S\| < s)) \leftrightarrow (\forall z \in A (a \leq z \to \|B - R\| < r) \land \forall z \in A (b \leq z \to \|C - S\| < s))$
21		anim12	$⊢ ((a \leq z \to \|B - R\| < r) \land (b \leq z \to \|C - S\| < s)) \to ((a \leq z \land b \leq z) \to (\|B - R\| < r \land \|C - S\| < s))$
22		simplrl	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to a \in ℝ$
23		simplrr	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to b \in ℝ$
24		eqid	$⊢ (z \in A ⟼ B) = (z \in A ⟼ B)$
25	24 1	dmmptd	$⊢ φ \to dom (z \in A ⟼ B) = A$
26		rlimss	$⊢ (z \in A ⟼ B) \underset{ℝ}{⇝} R \to dom (z \in A ⟼ B) \subseteq ℝ$
27	5 26	syl	$⊢ φ \to dom (z \in A ⟼ B) \subseteq ℝ$
28	25 27	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
29	28	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to A \subseteq ℝ$
30	29	sselda	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to z \in ℝ$
31		maxle	$⊢ (a \in ℝ \land b \in ℝ \land z \in ℝ) \to (if (a \leq b, b, a) \leq z \leftrightarrow (a \leq z \land b \leq z))$
32	22 23 30 31	syl3anc	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to (if (a \leq b, b, a) \leq z \leftrightarrow (a \leq z \land b \leq z))$
33	32	imbi1d	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to ((if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \leftrightarrow ((a \leq z \land b \leq z) \to (\|B - R\| < r \land \|C - S\| < s)))$
34	21 33	syl5ibr	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land z \in A) \to (((a \leq z \to \|B - R\| < r) \land (b \leq z \to \|C - S\| < s)) \to (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)))$
35	34	ralimdva	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to (\forall z \in A ((a \leq z \to \|B - R\| < r) \land (b \leq z \to \|C - S\| < s)) \to \forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)))$
36		ifcl	$⊢ (b \in ℝ \land a \in ℝ) \to if (a \leq b, b, a) \in ℝ$
37	36	ancoms	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, b, a) \in ℝ$
38	37	ad2antlr	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to if (a \leq b, b, a) \in ℝ$
39	1	adantlr	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land z \in A) \to B \in X$
40	2	adantlr	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land z \in A) \to C \in Y$
41	39 40	jca	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land z \in A) \to (B \in X \land C \in Y)$
42		fvoveq1	$⊢ u = B \to \|u - R\| = \|B - R\|$
43	42	breq1d	$⊢ u = B \to (\|u - R\| < r \leftrightarrow \|B - R\| < r)$
44	43	anbi1d	$⊢ u = B \to ((\|u - R\| < r \land \|v - S\| < s) \leftrightarrow (\|B - R\| < r \land \|v - S\| < s))$
45		oveq1	$⊢ u = B \to u F v = B F v$
46	45	fvoveq1d	$⊢ u = B \to \|(u F v) - (R F S)\| = \|(B F v) - (R F S)\|$
47	46	breq1d	$⊢ u = B \to (\|(u F v) - (R F S)\| < x \leftrightarrow \|(B F v) - (R F S)\| < x)$
48	44 47	imbi12d	$⊢ u = B \to (((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \leftrightarrow ((\|B - R\| < r \land \|v - S\| < s) \to \|(B F v) - (R F S)\| < x))$
49		fvoveq1	$⊢ v = C \to \|v - S\| = \|C - S\|$
50	49	breq1d	$⊢ v = C \to (\|v - S\| < s \leftrightarrow \|C - S\| < s)$
51	50	anbi2d	$⊢ v = C \to ((\|B - R\| < r \land \|v - S\| < s) \leftrightarrow (\|B - R\| < r \land \|C - S\| < s))$
52		oveq2	$⊢ v = C \to B F v = B F C$
53	52	fvoveq1d	$⊢ v = C \to \|(B F v) - (R F S)\| = \|(B F C) - (R F S)\|$
54	53	breq1d	$⊢ v = C \to (\|(B F v) - (R F S)\| < x \leftrightarrow \|(B F C) - (R F S)\| < x)$
55	51 54	imbi12d	$⊢ v = C \to (((\|B - R\| < r \land \|v - S\| < s) \to \|(B F v) - (R F S)\| < x) \leftrightarrow ((\|B - R\| < r \land \|C - S\| < s) \to \|(B F C) - (R F S)\| < x))$
56	48 55	rspc2va	$⊢ ((B \in X \land C \in Y) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to ((\|B - R\| < r \land \|C - S\| < s) \to \|(B F C) - (R F S)\| < x)$
57	41 56	sylan	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land z \in A) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to ((\|B - R\| < r \land \|C - S\| < s) \to \|(B F C) - (R F S)\| < x)$
58	57	imim2d	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land z \in A) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to ((if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to (if (a \leq b, b, a) \leq z \to \|(B F C) - (R F S)\| < x))$
59	58	an32s	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \land z \in A) \to ((if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to (if (a \leq b, b, a) \leq z \to \|(B F C) - (R F S)\| < x))$
60	59	ralimdva	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to (\forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to \forall z \in A (if (a \leq b, b, a) \leq z \to \|(B F C) - (R F S)\| < x))$
61	60	adantlr	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to (\forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to \forall z \in A (if (a \leq b, b, a) \leq z \to \|(B F C) - (R F S)\| < x))$
62		breq1	$⊢ c = if (a \leq b, b, a) \to (c \leq z \leftrightarrow if (a \leq b, b, a) \leq z)$
63	62	rspceaimv	$⊢ (if (a \leq b, b, a) \in ℝ \land \forall z \in A (if (a \leq b, b, a) \leq z \to \|(B F C) - (R F S)\| < x)) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)$
64	38 61 63	syl6an	$⊢ (((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \land \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to (\forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x))$
65	64	ex	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to (\forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
66	65	com23	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to (\forall z \in A (if (a \leq b, b, a) \leq z \to (\|B - R\| < r \land \|C - S\| < s)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
67	35 66	syld	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to (\forall z \in A ((a \leq z \to \|B - R\| < r) \land (b \leq z \to \|C - S\| < s)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
68	20 67	syl5bir	$⊢ ((φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \land (a \in ℝ \land b \in ℝ)) \to ((\forall z \in A (a \leq z \to \|B - R\| < r) \land \forall z \in A (b \leq z \to \|C - S\| < s)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
69	68	rexlimdvva	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to (\exists a \in ℝ \exists b \in ℝ (\forall z \in A (a \leq z \to \|B - R\| < r) \land \forall z \in A (b \leq z \to \|C - S\| < s)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
70	19 69	syl5bir	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to ((\exists a \in ℝ \forall z \in A (a \leq z \to \|B - R\| < r) \land \exists b \in ℝ \forall z \in A (b \leq z \to \|C - S\| < s)) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)))$
71	13 18 70	mp2and	$⊢ (φ \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to (\forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x))$
72	71	rexlimdvva	$⊢ φ \to (\exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x))$
73	72	imp	$⊢ (φ \land \exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)$
74	8 73	syldan	$⊢ (φ \land x \in ℝ^{+}) \to \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)$
75	74	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x)$
76	7	adantr	$⊢ (φ \land z \in A) \to F : X \times Y ⟶ ℂ$
77	76 1 2	fovrnd	$⊢ (φ \land z \in A) \to B F C \in ℂ$
78	77	ralrimiva	$⊢ φ \to \forall z \in A B F C \in ℂ$
79	7 3 4	fovrnd	$⊢ φ \to R F S \in ℂ$
80	78 28 79	rlim2	$⊢ φ \to ((z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S) \leftrightarrow \forall x \in ℝ^{+} \exists c \in ℝ \forall z \in A (c \leq z \to \|(B F C) - (R F S)\| < x))$
81	75 80	mpbird	$⊢ φ \to (z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S)$

Metamath Proof Explorer

Theorem rlimcn2

Proof