Metamath Proof Explorer

Theorem cnllycmp

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

Ref Expression
Hypothesis cnllycmp.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion cnllycmp 𝐽 ∈ 𝑛-Locally Comp

Proof

Step Hyp Ref Expression
1 cnllycmp.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 1 cnfldtop ⊢ 𝐽 ∈ Top
3 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
4 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
5 4 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
6 3 5 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
7 2 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝐽 ∈ Top )
8 3 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
9 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
10 9 ad2antrr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ ∪ 𝐽 )
11 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
12 11 toponunii ⊢ ℂ = ∪ 𝐽
13 10 12 sseqtrrdi ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ ℂ )
14 simplr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
15 13 14 sseldd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ ℂ )
16 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
17 16 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
18 17 rpxrd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑟 / 2 ) ∈ ℝ* )
19 4 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
20 8 15 18 19 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
21 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) )
22 8 15 17 21 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) )
23 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
24 7 20 22 23 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
25 blssm ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ℂ )
26 8 15 18 25 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ℂ )
27 12 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ℂ ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) )
28 7 26 27 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) )
29 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
30 29 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → 𝑟 ∈ ℝ* )
31 rphalflt ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) < 𝑟 )
32 31 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑟 / 2 ) < 𝑟 )
33 4 blsscls ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ) ∧ ( ( 𝑟 / 2 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ ( 𝑟 / 2 ) < 𝑟 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
34 8 15 18 30 32 33 syl23anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
35 simprr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 )
36 34 35 sstrd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ 𝑥 )
37 36 13 sstrd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ ℂ )
38 12 ssnei2 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) ∧ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ ℂ ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
39 7 24 28 37 38 syl22anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
40 vex ⊢ 𝑥 ∈ V
41 40 elpw2 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ 𝒫 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ 𝑥 )
42 36 41 sylibr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ 𝒫 𝑥 )
43 39 42 elind ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
44 12 clscld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ⊆ ℂ ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
45 7 26 44 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
46 15 abscld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( abs ‘ 𝑦 ) ∈ ℝ )
47 17 rpred ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝑟 / 2 ) ∈ ℝ )
48 46 47 readdcld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ∈ ℝ )
49 eqid ⊢ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } = { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) }
50 4 49 blcls ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } )
51 8 15 18 50 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } )
52 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
53 15 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑦 ∈ ℂ )
54 52 53 abs2difd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
55 52 abscld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ 𝑧 ) ∈ ℝ )
56 46 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ 𝑦 ) ∈ ℝ )
57 55 56 resubcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ∈ ℝ )
58 52 53 subcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 − 𝑦 ) ∈ ℂ )
59 58 abscld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) ∈ ℝ )
60 47 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑟 / 2 ) ∈ ℝ )
61 letr ⊢ ( ( ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ ) → ( ( ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) ≤ ( 𝑟 / 2 ) ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( 𝑟 / 2 ) ) )
62 57 59 60 61 syl3anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) ≤ ( 𝑟 / 2 ) ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( 𝑟 / 2 ) ) )
63 54 62 mpand ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) ≤ ( 𝑟 / 2 ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( 𝑟 / 2 ) ) )
64 52 53 abssubd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
65 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
66 65 cnmetdval ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
67 15 66 sylan ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
68 64 67 eqtr4d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( 𝑦 ( abs ∘ − ) 𝑧 ) )
69 68 breq1d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) ≤ ( 𝑟 / 2 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑧 ) ≤ ( 𝑟 / 2 ) ) )
70 55 56 60 lesubadd2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝑦 ) ) ≤ ( 𝑟 / 2 ) ↔ ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) )
71 63 69 70 3imtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑦 ( abs ∘ − ) 𝑧 ) ≤ ( 𝑟 / 2 ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) )
72 71 ralrimiva ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∀ 𝑧 ∈ ℂ ( ( 𝑦 ( abs ∘ − ) 𝑧 ) ≤ ( 𝑟 / 2 ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) )
73 oveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ( abs ∘ − ) 𝑤 ) = ( 𝑦 ( abs ∘ − ) 𝑧 ) )
74 73 breq1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑧 ) ≤ ( 𝑟 / 2 ) ) )
75 74 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ↔ ∀ 𝑧 ∈ ℂ ( ( 𝑦 ( abs ∘ − ) 𝑧 ) ≤ ( 𝑟 / 2 ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) )
76 72 75 sylibr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∀ 𝑧 ∈ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) )
77 ssralv ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } → ( ∀ 𝑧 ∈ { 𝑤 ∈ ℂ ∣ ( 𝑦 ( abs ∘ − ) 𝑤 ) ≤ ( 𝑟 / 2 ) } ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) → ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) )
78 51 76 77 sylc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) )
79 brralrspcev ⊢ ( ( ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ∈ ℝ ∧ ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑦 ) + ( 𝑟 / 2 ) ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ 𝑠 )
80 48 78 79 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ 𝑠 )
81 eqid ⊢ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) = ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) )
82 1 81 cnheibor ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ⊆ ℂ → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) ∈ Comp ↔ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ 𝑠 ) ) )
83 37 82 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) ∈ Comp ↔ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ( abs ‘ 𝑧 ) ≤ 𝑠 ) ) )
84 45 80 83 mpbir2and ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) ∈ Comp )
85 oveq2 ⊢ ( 𝑢 = ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) → ( 𝐽 ↾t 𝑢 ) = ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) )
86 85 eleq1d ⊢ ( 𝑢 = ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) → ( ( 𝐽 ↾t 𝑢 ) ∈ Comp ↔ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) ∈ Comp ) )
87 86 rspcev ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) ( 𝑟 / 2 ) ) ) ) ∈ Comp ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ Comp )
88 43 84 87 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑥 ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ Comp )
89 6 88 rexlimddv ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ Comp )
90 89 rgen2 ⊢ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ Comp
91 isnlly ⊢ ( 𝐽 ∈ 𝑛-Locally Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ Comp ) )
92 2 90 91 mpbir2an ⊢ 𝐽 ∈ 𝑛-Locally Comp