Step | Hyp | Ref
| Expression |
1 | | cnxmet 22386 |
. . . . . . 7
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
2 | | reperflem.3 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℂ |
3 | 2 | sseli 3564 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ) |
4 | | recld2.1 |
. . . . . . . . 9
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | cnfldtopn 22395 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
6 | 5 | neibl 22116 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ ℂ) → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
7 | 1, 3, 6 | sylancr 694 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
8 | | reperflem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆) |
9 | 8 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → ∀𝑣 ∈ ℝ (𝑢 + 𝑣) ∈ 𝑆) |
10 | | rpre 11715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
11 | 10 | rehalfcld 11156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
12 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑟 / 2) → (𝑢 + 𝑣) = (𝑢 + (𝑟 / 2))) |
13 | 12 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑟 / 2) → ((𝑢 + 𝑣) ∈ 𝑆 ↔ (𝑢 + (𝑟 / 2)) ∈ 𝑆)) |
14 | 13 | rspccva 3281 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑣 ∈
ℝ (𝑢 + 𝑣) ∈ 𝑆 ∧ (𝑟 / 2) ∈ ℝ) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
15 | 9, 11, 14 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
16 | 2, 15 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ ℂ) |
17 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑢 ∈
ℂ) |
18 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
19 | 18 | cnmetdval 22384 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 + (𝑟 / 2)) ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
20 | 16, 17, 19 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
21 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
22 | 21 | rphalfcld 11760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
23 | 22 | rpcnd 11750 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℂ) |
24 | 17, 23 | pncan2d 10273 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) = (𝑟 / 2)) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘((𝑢 + (𝑟 / 2)) − 𝑢)) = (abs‘(𝑟 / 2))) |
26 | 22 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ) |
27 | 22 | rpge0d 11752 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(𝑟 / 2)) |
28 | 26, 27 | absidd 14009 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘(𝑟 / 2)) =
(𝑟 / 2)) |
29 | 20, 25, 28 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (𝑟 / 2)) |
30 | | rphalflt 11736 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
31 | 30 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟) |
32 | 29, 31 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟) |
33 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
34 | | rpxr 11716 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
35 | 34 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
36 | | elbl3 22007 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑢 ∈ ℂ ∧ (𝑢 + (𝑟 / 2)) ∈ ℂ)) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
37 | 33, 35, 17, 16, 36 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
38 | 32, 37 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟)) |
39 | 22 | rpne0d 11753 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ≠ 0) |
40 | 24, 39 | eqnetrd 2849 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) ≠ 0) |
41 | 16, 17, 40 | subne0ad 10282 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ≠ 𝑢) |
42 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ ((𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢}) ↔ ((𝑢 + (𝑟 / 2)) ∈ 𝑆 ∧ (𝑢 + (𝑟 / 2)) ≠ 𝑢)) |
43 | 15, 41, 42 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) |
44 | | inelcm 3984 |
. . . . . . . . . 10
⊢ (((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ∧ (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
45 | 38, 43, 44 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
46 | | ssrin 3800 |
. . . . . . . . . 10
⊢ ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢}))) |
47 | | ssn0 3928 |
. . . . . . . . . . 11
⊢ ((((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢})) ∧ ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
48 | 47 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢})) → (((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅ → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
49 | 46, 48 | syl 17 |
. . . . . . . . 9
⊢ ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅ → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
50 | 45, 49 | syl5com 31 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
51 | 50 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → (∃𝑟 ∈ ℝ+ (𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
52 | 51 | adantld 482 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → ((𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
53 | 7, 52 | sylbid 229 |
. . . . 5
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
54 | 53 | ralrimiv 2948 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
55 | 4 | cnfldtop 22397 |
. . . . . 6
⊢ 𝐽 ∈ Top |
56 | 4 | cnfldtopon 22396 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
57 | 56 | toponunii 20547 |
. . . . . . 7
⊢ ℂ =
∪ 𝐽 |
58 | 57 | islp2 20759 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ ∧ 𝑢 ∈ ℂ) → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
59 | 55, 2, 58 | mp3an12 1406 |
. . . . 5
⊢ (𝑢 ∈ ℂ → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
60 | 3, 59 | syl 17 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
61 | 54, 60 | mpbird 246 |
. . 3
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ((limPt‘𝐽)‘𝑆)) |
62 | 61 | ssriv 3572 |
. 2
⊢ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆) |
63 | | eqid 2610 |
. . . 4
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
64 | 57, 63 | restperf 20798 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆))) |
65 | 55, 2, 64 | mp2an 704 |
. 2
⊢ ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)) |
66 | 62, 65 | mpbir 220 |
1
⊢ (𝐽 ↾t 𝑆) ∈ Perf |