rlimcn3

Description: Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 . (Contributed by SN, 27-Sep-2024)

	Ref	Expression
Hypotheses	rlimcn3.1a	$⊢ (φ \land z \in A) \to B \in X$
	rlimcn3.1b	$⊢ (φ \land z \in A) \to C \in Y$
	rlimcn3.1c	$⊢ (φ \land z \in A) \to B F C \in ℂ$
	rlimcn3.2	$⊢ φ \to R F S \in ℂ$
	rlimcn3.3a	$⊢ φ \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
	rlimcn3.3b	$⊢ φ \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
	rlimcn3.4	$⊢ (φ \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	rlimcn3	$⊢ φ \to (z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S)$

Proof

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

Metamath Proof Explorer

Theorem rlimcn3

Proof