cnllycmp

Description: The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Hypothesis	cnllycmp.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	cnllycmp	$⊢ J \in N-LocallyComp$

Proof

Step	Hyp	Ref	Expression
1		cnllycmp.1	$⊢ J = TopOpen (ℂ_{fld})$
2	1	cnfldtop	$⊢ J \in Top$
3		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
4	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
5	4	mopni2	$⊢ (abs \circ - \in ∞Met (ℂ) \land x \in J \land y \in x) \to \exists r \in ℝ^{+} y ball (abs \circ -) r \subseteq x$
6	3 5	mp3an1	$⊢ (x \in J \land y \in x) \to \exists r \in ℝ^{+} y ball (abs \circ -) r \subseteq x$
7	2	a1i	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to J \in Top$
8	3	a1i	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to abs \circ - \in ∞Met (ℂ)$
9		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
10	9	ad2antrr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to x \subseteq ⋃ J$
11	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
12	11	toponunii	$⊢ ℂ = ⋃ J$
13	10 12	sseqtrrdi	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to x \subseteq ℂ$
14		simplr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in x$
15	13 14	sseldd	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in ℂ$
16		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
17	16	ad2antrl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \frac{r}{2} \in ℝ^{+}$
18	17	rpxrd	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \frac{r}{2} \in ℝ^{*}$
19	4	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land \frac{r}{2} \in ℝ^{*}) \to y ball (abs \circ -) (\frac{r}{2}) \in J$
20	8 15 18 19	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) (\frac{r}{2}) \in J$
21		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land \frac{r}{2} \in ℝ^{+}) \to y \in (y ball (abs \circ -) (\frac{r}{2}))$
22	8 15 17 21	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y \in (y ball (abs \circ -) (\frac{r}{2}))$
23		opnneip	$⊢ (J \in Top \land y ball (abs \circ -) (\frac{r}{2}) \in J \land y \in (y ball (abs \circ -) (\frac{r}{2}))) \to y ball (abs \circ -) (\frac{r}{2}) \in nei (J) (\{y\})$
24	7 20 22 23	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) (\frac{r}{2}) \in nei (J) (\{y\})$
25		blssm	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land \frac{r}{2} \in ℝ^{*}) \to y ball (abs \circ -) (\frac{r}{2}) \subseteq ℂ$
26	8 15 18 25	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) (\frac{r}{2}) \subseteq ℂ$
27	12	sscls	$⊢ (J \in Top \land y ball (abs \circ -) (\frac{r}{2}) \subseteq ℂ) \to y ball (abs \circ -) (\frac{r}{2}) \subseteq cls (J) (y ball (abs \circ -) (\frac{r}{2}))$
28	7 26 27	syl2anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) (\frac{r}{2}) \subseteq cls (J) (y ball (abs \circ -) (\frac{r}{2}))$
29		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
30	29	ad2antrl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to r \in ℝ^{*}$
31		rphalflt	$⊢ r \in ℝ^{+} \to \frac{r}{2} < r$
32	31	ad2antrl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \frac{r}{2} < r$
33	4	blsscls	$⊢ ((abs \circ - \in ∞Met (ℂ) \land y \in ℂ) \land (\frac{r}{2} \in ℝ^{} \land r \in ℝ^{} \land \frac{r}{2} < r)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq y ball (abs \circ -) r$
34	8 15 18 30 32 33	syl23anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq y ball (abs \circ -) r$
35		simprr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to y ball (abs \circ -) r \subseteq x$
36	34 35	sstrd	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq x$
37	36 13	sstrd	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq ℂ$
38	12	ssnei2	$⊢ ((J \in Top \land y ball (abs \circ -) (\frac{r}{2}) \in nei (J) (\{y\})) \land (y ball (abs \circ -) (\frac{r}{2}) \subseteq cls (J) (y ball (abs \circ -) (\frac{r}{2})) \land cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq ℂ)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in nei (J) (\{y\})$
39	7 24 28 37 38	syl22anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in nei (J) (\{y\})$
40		vex	$⊢ x \in V$
41	40	elpw2	$⊢ cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in 𝒫 x \leftrightarrow cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq x$
42	36 41	sylibr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in 𝒫 x$
43	39 42	elind	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in (nei (J) (\{y\}) \cap 𝒫 x)$
44	12	clscld	$⊢ (J \in Top \land y ball (abs \circ -) (\frac{r}{2}) \subseteq ℂ) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Clsd (J)$
45	7 26 44	syl2anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Clsd (J)$
46	15	abscld	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \|y\| \in ℝ$
47	17	rpred	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \frac{r}{2} \in ℝ$
48	46 47	readdcld	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \|y\| + (\frac{r}{2}) \in ℝ$
49		eqid	$⊢ \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\} = \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\}$
50	4 49	blcls	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land \frac{r}{2} \in ℝ^{*}) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\}$
51	8 15 18 50	syl3anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\}$
52		simpr	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to z \in ℂ$
53	15	adantr	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to y \in ℂ$
54	52 53	abs2difd	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z\| - \|y\| \leq \|z - y\|$
55	52	abscld	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z\| \in ℝ$
56	46	adantr	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|y\| \in ℝ$
57	55 56	resubcld	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z\| - \|y\| \in ℝ$
58	52 53	subcld	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to z - y \in ℂ$
59	58	abscld	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z - y\| \in ℝ$
60	47	adantr	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \frac{r}{2} \in ℝ$
61		letr	$⊢ (\|z\| - \|y\| \in ℝ \land \|z - y\| \in ℝ \land \frac{r}{2} \in ℝ) \to ((\|z\| - \|y\| \leq \|z - y\| \land \|z - y\| \leq \frac{r}{2}) \to \|z\| - \|y\| \leq \frac{r}{2})$
62	57 59 60 61	syl3anc	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to ((\|z\| - \|y\| \leq \|z - y\| \land \|z - y\| \leq \frac{r}{2}) \to \|z\| - \|y\| \leq \frac{r}{2})$
63	54 62	mpand	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to (\|z - y\| \leq \frac{r}{2} \to \|z\| - \|y\| \leq \frac{r}{2})$
64	52 53	abssubd	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z - y\| = \|y - z\|$
65		eqid	$⊢ abs \circ - = abs \circ -$
66	65	cnmetdval	$⊢ (y \in ℂ \land z \in ℂ) \to y (abs \circ -) z = \|y - z\|$
67	15 66	sylan	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to y (abs \circ -) z = \|y - z\|$
68	64 67	eqtr4d	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to \|z - y\| = y (abs \circ -) z$
69	68	breq1d	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to (\|z - y\| \leq \frac{r}{2} \leftrightarrow y (abs \circ -) z \leq \frac{r}{2})$
70	55 56 60	lesubadd2d	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to (\|z\| - \|y\| \leq \frac{r}{2} \leftrightarrow \|z\| \leq \|y\| + (\frac{r}{2}))$
71	63 69 70	3imtr3d	$⊢ (((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \land z \in ℂ) \to (y (abs \circ -) z \leq \frac{r}{2} \to \|z\| \leq \|y\| + (\frac{r}{2}))$
72	71	ralrimiva	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \forall z \in ℂ (y (abs \circ -) z \leq \frac{r}{2} \to \|z\| \leq \|y\| + (\frac{r}{2}))$
73		oveq2	$⊢ w = z \to y (abs \circ -) w = y (abs \circ -) z$
74	73	breq1d	$⊢ w = z \to (y (abs \circ -) w \leq \frac{r}{2} \leftrightarrow y (abs \circ -) z \leq \frac{r}{2})$
75	74	ralrab	$⊢ \forall z \in \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\} \|z\| \leq \|y\| + (\frac{r}{2}) \leftrightarrow \forall z \in ℂ (y (abs \circ -) z \leq \frac{r}{2} \to \|z\| \leq \|y\| + (\frac{r}{2}))$
76	72 75	sylibr	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \forall z \in \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\} \|z\| \leq \|y\| + (\frac{r}{2})$
77		ssralv	$⊢ cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\} \to (\forall z \in \{w \in ℂ \| y (abs \circ -) w \leq \frac{r}{2}\} \|z\| \leq \|y\| + (\frac{r}{2}) \to \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq \|y\| + (\frac{r}{2}))$
78	51 76 77	sylc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq \|y\| + (\frac{r}{2})$
79		brralrspcev	$⊢ (\|y\| + (\frac{r}{2}) \in ℝ \land \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq \|y\| + (\frac{r}{2})) \to \exists s \in ℝ \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq s$
80	48 78 79	syl2anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \exists s \in ℝ \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq s$
81		eqid	$⊢ J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) = J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2}))$
82	1 81	cnheibor	$⊢ cls (J) (y ball (abs \circ -) (\frac{r}{2})) \subseteq ℂ \to (J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Comp \leftrightarrow (cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Clsd (J) \land \exists s \in ℝ \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq s))$
83	37 82	syl	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to (J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Comp \leftrightarrow (cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Clsd (J) \land \exists s \in ℝ \forall z \in cls (J) (y ball (abs \circ -) (\frac{r}{2})) \|z\| \leq s))$
84	45 80 83	mpbir2and	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Comp$
85		oveq2	$⊢ u = cls (J) (y ball (abs \circ -) (\frac{r}{2})) \to J ↾_{𝑡} u = J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2}))$
86	85	eleq1d	$⊢ u = cls (J) (y ball (abs \circ -) (\frac{r}{2})) \to (J ↾_{𝑡} u \in Comp \leftrightarrow J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Comp)$
87	86	rspcev	$⊢ (cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in (nei (J) (\{y\}) \cap 𝒫 x) \land J ↾_{𝑡} cls (J) (y ball (abs \circ -) (\frac{r}{2})) \in Comp) \to \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in Comp$
88	43 84 87	syl2anc	$⊢ ((x \in J \land y \in x) \land (r \in ℝ^{+} \land y ball (abs \circ -) r \subseteq x)) \to \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in Comp$
89	6 88	rexlimddv	$⊢ (x \in J \land y \in x) \to \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in Comp$
90	89	rgen2	$⊢ \forall x \in J \forall y \in x \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in Comp$
91		isnlly	$⊢ J \in N-LocallyComp\leftrightarrow(J \in Top \land \forall x \in J)$
92	2 90 91	mpbir2an	$⊢ J \in N-LocallyComp$

Metamath Proof Explorer

Theorem cnllycmp

Proof