Step | Hyp | Ref
| Expression |
1 | | cnxmet 22576 |
. . . . . . 7
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
2 | | reperflem.3 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℂ |
3 | 2 | sseli 3599 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ) |
4 | | recld2.1 |
. . . . . . . . 9
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | cnfldtopn 22585 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
6 | 5 | neibl 22306 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ ℂ) → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
7 | 1, 3, 6 | sylancr 695 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
8 | | reperflem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆) |
9 | 8 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → ∀𝑣 ∈ ℝ (𝑢 + 𝑣) ∈ 𝑆) |
10 | | rpre 11839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
11 | 10 | rehalfcld 11279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
12 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑟 / 2) → (𝑢 + 𝑣) = (𝑢 + (𝑟 / 2))) |
13 | 12 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑟 / 2) → ((𝑢 + 𝑣) ∈ 𝑆 ↔ (𝑢 + (𝑟 / 2)) ∈ 𝑆)) |
14 | 13 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑣 ∈
ℝ (𝑢 + 𝑣) ∈ 𝑆 ∧ (𝑟 / 2) ∈ ℝ) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
15 | 9, 11, 14 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
16 | 2, 15 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ ℂ) |
17 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑢 ∈
ℂ) |
18 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
19 | 18 | cnmetdval 22574 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 + (𝑟 / 2)) ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
20 | 16, 17, 19 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
21 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
22 | 21 | rphalfcld 11884 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
23 | 22 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℂ) |
24 | 17, 23 | pncan2d 10394 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) = (𝑟 / 2)) |
25 | 24 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘((𝑢 + (𝑟 / 2)) − 𝑢)) = (abs‘(𝑟 / 2))) |
26 | 22 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ) |
27 | 22 | rpge0d 11876 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(𝑟 / 2)) |
28 | 26, 27 | absidd 14161 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘(𝑟 / 2)) =
(𝑟 / 2)) |
29 | 20, 25, 28 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (𝑟 / 2)) |
30 | | rphalflt 11860 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
31 | 30 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟) |
32 | 29, 31 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟) |
33 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
34 | | rpxr 11840 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
35 | 34 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
36 | | elbl3 22197 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑢 ∈ ℂ ∧ (𝑢 + (𝑟 / 2)) ∈ ℂ)) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
37 | 33, 35, 17, 16, 36 | syl22anc 1327 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
38 | 32, 37 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟)) |
39 | 22 | rpne0d 11877 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ≠ 0) |
40 | 24, 39 | eqnetrd 2861 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) ≠ 0) |
41 | 16, 17, 40 | subne0ad 10403 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ≠ 𝑢) |
42 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ ((𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢}) ↔ ((𝑢 + (𝑟 / 2)) ∈ 𝑆 ∧ (𝑢 + (𝑟 / 2)) ≠ 𝑢)) |
43 | 15, 41, 42 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) |
44 | | inelcm 4032 |
. . . . . . . . . 10
⊢ (((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ∧ (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
45 | 38, 43, 44 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
46 | | ssrin 3838 |
. . . . . . . . . 10
⊢ ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢}))) |
47 | | ssn0 3976 |
. . . . . . . . . . 11
⊢ ((((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢})) ∧ ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
48 | 47 | ex 450 |
. . . . . . . . . 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 3031 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → (∃𝑟 ∈ ℝ+ (𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
52 | 51 | adantld 483 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → ((𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
53 | 7, 52 | sylbid 230 |
. . . . 5
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
54 | 53 | ralrimiv 2965 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
55 | 4 | cnfldtop 22587 |
. . . . . 6
⊢ 𝐽 ∈ Top |
56 | 4 | cnfldtopon 22586 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
57 | 56 | toponunii 20721 |
. . . . . . 7
⊢ ℂ =
∪ 𝐽 |
58 | 57 | islp2 20949 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ ∧ 𝑢 ∈ ℂ) → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
59 | 55, 2, 58 | mp3an12 1414 |
. . . . 5
⊢ (𝑢 ∈ ℂ → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
60 | 3, 59 | syl 17 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
61 | 54, 60 | mpbird 247 |
. . 3
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ((limPt‘𝐽)‘𝑆)) |
62 | 61 | ssriv 3607 |
. 2
⊢ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆) |
63 | | eqid 2622 |
. . . 4
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
64 | 57, 63 | restperf 20988 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆))) |
65 | 55, 2, 64 | mp2an 708 |
. 2
⊢ ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)) |
66 | 62, 65 | mpbir 221 |
1
⊢ (𝐽 ↾t 𝑆) ∈ Perf |