addcnlem

	Ref	Expression
Hypotheses	addcn.j	$⊢ J = TopOpen (ℂ_{fld})$
	addcn.2	$⊢ \underset{˙}{+} : ℂ \times ℂ ⟶ ℂ$
	addcn.3	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a)$
Assertion	addcnlem	$⊢ \underset{˙}{+} \in ((J \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		addcn.j	$⊢ J = TopOpen (ℂ_{fld})$
2		addcn.2	$⊢ \underset{˙}{+} : ℂ \times ℂ ⟶ ℂ$
3		addcn.3	$⊢ (a \in ℝ^{+} \land b \in ℂ \land c \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a)$
4	3	3coml	$⊢ (b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a)$
5		ifcl	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to if (y \leq z, y, z) \in ℝ^{+}$
6	5	adantl	$⊢ ((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to if (y \leq z, y, z) \in ℝ^{+}$
7		simpll1	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to b \in ℂ$
8		simprl	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to u \in ℂ$
9		eqid	$⊢ abs \circ - = abs \circ -$
10	9	cnmetdval	$⊢ (b \in ℂ \land u \in ℂ) \to b (abs \circ -) u = \|b - u\|$
11		abssub	$⊢ (b \in ℂ \land u \in ℂ) \to \|b - u\| = \|u - b\|$
12	10 11	eqtrd	$⊢ (b \in ℂ \land u \in ℂ) \to b (abs \circ -) u = \|u - b\|$
13	7 8 12	syl2anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to b (abs \circ -) u = \|u - b\|$
14	13	breq1d	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (b (abs \circ -) u < if (y \leq z, y, z) \leftrightarrow \|u - b\| < if (y \leq z, y, z))$
15	8 7	subcld	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to u - b \in ℂ$
16	15	abscld	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to \|u - b\| \in ℝ$
17		simplrl	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to y \in ℝ^{+}$
18	17	rpred	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to y \in ℝ$
19		simplrr	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to z \in ℝ^{+}$
20	19	rpred	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to z \in ℝ$
21		ltmin	$⊢ (\|u - b\| \in ℝ \land y \in ℝ \land z \in ℝ) \to (\|u - b\| < if (y \leq z, y, z) \leftrightarrow (\|u - b\| < y \land \|u - b\| < z))$
22	16 18 20 21	syl3anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (\|u - b\| < if (y \leq z, y, z) \leftrightarrow (\|u - b\| < y \land \|u - b\| < z))$
23	14 22	bitrd	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (b (abs \circ -) u < if (y \leq z, y, z) \leftrightarrow (\|u - b\| < y \land \|u - b\| < z))$
24		simpl	$⊢ (\|u - b\| < y \land \|u - b\| < z) \to \|u - b\| < y$
25	23 24	syl6bi	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (b (abs \circ -) u < if (y \leq z, y, z) \to \|u - b\| < y)$
26		simpll2	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to c \in ℂ$
27		simprr	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to v \in ℂ$
28	9	cnmetdval	$⊢ (c \in ℂ \land v \in ℂ) \to c (abs \circ -) v = \|c - v\|$
29		abssub	$⊢ (c \in ℂ \land v \in ℂ) \to \|c - v\| = \|v - c\|$
30	28 29	eqtrd	$⊢ (c \in ℂ \land v \in ℂ) \to c (abs \circ -) v = \|v - c\|$
31	26 27 30	syl2anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to c (abs \circ -) v = \|v - c\|$
32	31	breq1d	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (c (abs \circ -) v < if (y \leq z, y, z) \leftrightarrow \|v - c\| < if (y \leq z, y, z))$
33	27 26	subcld	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to v - c \in ℂ$
34	33	abscld	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to \|v - c\| \in ℝ$
35		ltmin	$⊢ (\|v - c\| \in ℝ \land y \in ℝ \land z \in ℝ) \to (\|v - c\| < if (y \leq z, y, z) \leftrightarrow (\|v - c\| < y \land \|v - c\| < z))$
36	34 18 20 35	syl3anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (\|v - c\| < if (y \leq z, y, z) \leftrightarrow (\|v - c\| < y \land \|v - c\| < z))$
37	32 36	bitrd	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (c (abs \circ -) v < if (y \leq z, y, z) \leftrightarrow (\|v - c\| < y \land \|v - c\| < z))$
38		simpr	$⊢ (\|v - c\| < y \land \|v - c\| < z) \to \|v - c\| < z$
39	37 38	syl6bi	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (c (abs \circ -) v < if (y \leq z, y, z) \to \|v - c\| < z)$
40	25 39	anim12d	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (\|u - b\| < y \land \|v - c\| < z))$
41	2	fovcl	$⊢ (b \in ℂ \land c \in ℂ) \to b \underset{˙}{+} c \in ℂ$
42	7 26 41	syl2anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to b \underset{˙}{+} c \in ℂ$
43	2	fovcl	$⊢ (u \in ℂ \land v \in ℂ) \to u \underset{˙}{+} v \in ℂ$
44	43	adantl	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to u \underset{˙}{+} v \in ℂ$
45	9	cnmetdval	$⊢ (b \underset{˙}{+} c \in ℂ \land u \underset{˙}{+} v \in ℂ) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) = \|(b \underset{˙}{+} c) - (u \underset{˙}{+} v)\|$
46		abssub	$⊢ (b \underset{˙}{+} c \in ℂ \land u \underset{˙}{+} v \in ℂ) \to \|(b \underset{˙}{+} c) - (u \underset{˙}{+} v)\| = \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\|$
47	45 46	eqtrd	$⊢ (b \underset{˙}{+} c \in ℂ \land u \underset{˙}{+} v \in ℂ) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) = \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\|$
48	42 44 47	syl2anc	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) = \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\|$
49	48	breq1d	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to ((b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a \leftrightarrow \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a)$
50	49	biimprd	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (\|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)$
51	40 50	imim12d	$⊢ (((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land (u \in ℂ \land v \in ℂ)) \to (((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a) \to ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
52	51	ralimdvva	$⊢ ((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (\forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a) \to \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
53		breq2	$⊢ x = if (y \leq z, y, z) \to (b (abs \circ -) u < x \leftrightarrow b (abs \circ -) u < if (y \leq z, y, z))$
54		breq2	$⊢ x = if (y \leq z, y, z) \to (c (abs \circ -) v < x \leftrightarrow c (abs \circ -) v < if (y \leq z, y, z))$
55	53 54	anbi12d	$⊢ x = if (y \leq z, y, z) \to ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \leftrightarrow (b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)))$
56	55	imbi1d	$⊢ x = if (y \leq z, y, z) \to (((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a) \leftrightarrow ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
57	56	2ralbidv	$⊢ x = if (y \leq z, y, z) \to (\forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a) \leftrightarrow \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
58	57	rspcev	$⊢ (if (y \leq z, y, z) \in ℝ^{+} \land \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < if (y \leq z, y, z) \land c (abs \circ -) v < if (y \leq z, y, z)) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)) \to \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)$
59	6 52 58	syl6an	$⊢ ((b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (\forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a) \to \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
60	59	rexlimdvva	$⊢ (b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \to (\exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - b\| < y \land \|v - c\| < z) \to \|(u \underset{˙}{+} v) - (b \underset{˙}{+} c)\| < a) \to \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
61	4 60	mpd	$⊢ (b \in ℂ \land c \in ℂ \land a \in ℝ^{+}) \to \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)$
62	61	rgen3	$⊢ \forall b \in ℂ \forall c \in ℂ \forall a \in ℝ^{+} \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)$
63		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
64	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
65	64 64 64	txmetcn	$⊢ (abs \circ - \in ∞Met (ℂ) \land abs \circ - \in ∞Met (ℂ) \land abs \circ - \in ∞Met (ℂ)) \to (\underset{˙}{+} \in ((J \times_{t} J) Cn J) \leftrightarrow (\underset{˙}{+} : ℂ \times ℂ ⟶ ℂ \land \forall b \in ℂ \forall c \in ℂ \forall a \in ℝ^{+} \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a)))$
66	63 63 63 65	mp3an	$⊢ \underset{˙}{+} \in ((J \times_{t} J) Cn J) \leftrightarrow (\underset{˙}{+} : ℂ \times ℂ ⟶ ℂ \land \forall b \in ℂ \forall c \in ℂ \forall a \in ℝ^{+} \exists x \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((b (abs \circ -) u < x \land c (abs \circ -) v < x) \to (b \underset{˙}{+} c) (abs \circ -) (u \underset{˙}{+} v) < a))$
67	2 62 66	mpbir2an	$⊢ \underset{˙}{+} \in ((J \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem addcnlem

Proof