Step | Hyp | Ref
| Expression |
1 | | sumex 14835 |
. . . . . 6
⊢
Σ𝑗 ∈
ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V |
2 | 1 | rgenw 3106 |
. . . . 5
⊢
∀𝑦 ∈
𝑆 Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V |
3 | | pserf.f |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) |
4 | 3 | fnmpt 6268 |
. . . . 5
⊢
(∀𝑦 ∈
𝑆 Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V → 𝐹 Fn 𝑆) |
5 | 2, 4 | mp1i 13 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑆) |
6 | | psercn.s |
. . . . . . . . . . 11
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) |
7 | | cnvimass 5741 |
. . . . . . . . . . . 12
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
8 | | absf 14491 |
. . . . . . . . . . . . 13
⊢
abs:ℂ⟶ℝ |
9 | 8 | fdmi 6303 |
. . . . . . . . . . . 12
⊢ dom abs =
ℂ |
10 | 7, 9 | sseqtri 3856 |
. . . . . . . . . . 11
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
11 | 6, 10 | eqsstri 3854 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
ℂ |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
13 | 12 | sselda 3821 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
14 | | 0cn 10370 |
. . . . . . . . . . 11
⊢ 0 ∈
ℂ |
15 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) = (abs ∘ − ) |
16 | 15 | cnmetdval 22993 |
. . . . . . . . . . 11
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
17 | 14, 13, 16 | sylancr 581 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
18 | | abssub 14480 |
. . . . . . . . . . 11
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0))) |
19 | 14, 13, 18 | sylancr 581 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0))) |
20 | 13 | subid1d 10725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 − 0) = 𝑎) |
21 | 20 | fveq2d 6452 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘(𝑎 − 0)) = (abs‘𝑎)) |
22 | 17, 19, 21 | 3eqtrd 2818 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) = (abs‘𝑎)) |
23 | | breq2 4892 |
. . . . . . . . . . 11
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
24 | | breq2 4892 |
. . . . . . . . . . 11
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
25 | | simpr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
26 | 25, 6 | syl6eleq 2869 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (◡abs “ (0[,)𝑅))) |
27 | | ffn 6293 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
28 | | elpreima 6602 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs Fn
ℂ → (𝑎 ∈
(◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))) |
29 | 8, 27, 28 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) |
30 | 26, 29 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) |
31 | 30 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ (0[,)𝑅)) |
32 | | 0re 10380 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
33 | | iccssxr 12573 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ⊆ ℝ* |
34 | | pserf.g |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
35 | | pserf.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
36 | | pserf.r |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
37 | 34, 35, 36 | radcnvcl 24619 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
38 | 37 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈ (0[,]+∞)) |
39 | 33, 38 | sseldi 3819 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈
ℝ*) |
40 | | elico2 12554 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑅
∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
41 | 32, 39, 40 | sylancr 581 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
42 | 31, 41 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅)) |
43 | 42 | simp3d 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑅) |
44 | 43 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅) |
45 | 13 | abscld 14590 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
46 | | avglt1 11625 |
. . . . . . . . . . . . 13
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
47 | 45, 46 | sylan 575 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
48 | 44, 47 | mpbid 224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)) |
49 | 45 | ltp1d 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
50 | 49 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
51 | 23, 24, 48, 50 | ifbothda 4344 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))) |
52 | | psercn.m |
. . . . . . . . . 10
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) |
53 | 51, 52 | syl6breqr 4930 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
54 | 22, 53 | eqbrtrd 4910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) < 𝑀) |
55 | | cnxmet 22995 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
57 | 14 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℂ) |
58 | 34, 3, 35, 36, 6, 52 | psercnlem1 24627 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |
59 | 58 | simp1d 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
60 | 59 | rpxrd 12187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ*) |
61 | | elbl 22612 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑀 ∈
ℝ*) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs
∘ − )𝑎) <
𝑀))) |
62 | 56, 57, 60, 61 | syl3anc 1439 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs
∘ − )𝑎) <
𝑀))) |
63 | 13, 54, 62 | mpbir2and 703 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀)) |
64 | | fvres 6467 |
. . . . . . 7
⊢ (𝑎 ∈ (0(ball‘(abs
∘ − ))𝑀) →
((𝐹 ↾
(0(ball‘(abs ∘ − ))𝑀))‘𝑎) = (𝐹‘𝑎)) |
65 | 63, 64 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀))‘𝑎) = (𝐹‘𝑎)) |
66 | 3 | reseq1i 5640 |
. . . . . . . . . 10
⊢ (𝐹 ↾ (0(ball‘(abs
∘ − ))𝑀)) =
((𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ −
))𝑀)) |
67 | 34, 3, 35, 36, 6, 58 | psercnlem2 24626 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ (◡abs “ (0[,]𝑀)) ∧ (◡abs “ (0[,]𝑀)) ⊆ 𝑆)) |
68 | 67 | simp2d 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆ (◡abs “ (0[,]𝑀))) |
69 | 67 | simp3d 1135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡abs “ (0[,]𝑀)) ⊆ 𝑆) |
70 | 68, 69 | sstrd 3831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆ 𝑆) |
71 | 70 | resmptd 5704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ −
))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗))) |
72 | 66, 71 | syl5eq 2826 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗))) |
73 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ Σ𝑗 ∈
ℕ0 ((𝐺‘𝑦)‘𝑗)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) |
74 | 35 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
75 | | fveq2 6448 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑦 → (𝐺‘𝑘) = (𝐺‘𝑦)) |
76 | 75 | seqeq3d 13132 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑦 → seq0( + , (𝐺‘𝑘)) = seq0( + , (𝐺‘𝑦))) |
77 | 76 | fveq1d 6450 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (seq0( + , (𝐺‘𝑘))‘𝑠) = (seq0( + , (𝐺‘𝑦))‘𝑠)) |
78 | 77 | cbvmptv 4987 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ (seq0( + , (𝐺‘𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑠)) |
79 | | fveq2 6448 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑖 → (seq0( + , (𝐺‘𝑦))‘𝑠) = (seq0( + , (𝐺‘𝑦))‘𝑖)) |
80 | 79 | mpteq2dv 4982 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑖 → (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑖))) |
81 | 78, 80 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑖 → (𝑘 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑖))) |
82 | 81 | cbvmptv 4987 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℕ0
↦ (𝑘 ∈
(0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺‘𝑘))‘𝑠))) = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) |
83 | 59 | rpred 12186 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
84 | 58 | simp3d 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
85 | 34, 73, 74, 36, 82, 83, 84, 68 | psercn2 24625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) ∈ ((0(ball‘(abs ∘ −
))𝑀)–cn→ℂ)) |
86 | 72, 85 | eqeltrd 2859 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ)) |
87 | | cncff 23115 |
. . . . . . . 8
⊢ ((𝐹 ↾ (0(ball‘(abs
∘ − ))𝑀))
∈ ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)):(0(ball‘(abs
∘ − ))𝑀)⟶ℂ) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)):(0(ball‘(abs
∘ − ))𝑀)⟶ℂ) |
89 | 88, 63 | ffvelrnd 6626 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀))‘𝑎) ∈
ℂ) |
90 | 65, 89 | eqeltrrd 2860 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹‘𝑎) ∈ ℂ) |
91 | 90 | ralrimiva 3148 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (𝐹‘𝑎) ∈ ℂ) |
92 | | ffnfv 6654 |
. . . 4
⊢ (𝐹:𝑆⟶ℂ ↔ (𝐹 Fn 𝑆 ∧ ∀𝑎 ∈ 𝑆 (𝐹‘𝑎) ∈ ℂ)) |
93 | 5, 91, 92 | sylanbrc 578 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
94 | 70, 11 | syl6ss 3833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆
ℂ) |
95 | | ssid 3842 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
96 | | eqid 2778 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
97 | | eqid 2778 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t
(0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) |
98 | 96 | cnfldtopon 23005 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
99 | 98 | toponrestid 21144 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
100 | 96, 97, 99 | cncfcn 23131 |
. . . . . . . . 9
⊢
(((0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) |
101 | 94, 95, 100 | sylancl 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) |
102 | 86, 101 | eleqtrd 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) |
103 | 96 | cnfldtop 23006 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈ Top |
104 | 98 | toponunii 21139 |
. . . . . . . . . 10
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
105 | 104 | restuni 21385 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ) → (0(ball‘(abs
∘ − ))𝑀) =
∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀))) |
106 | 103, 94, 105 | sylancr 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) = ∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀))) |
107 | 63, 106 | eleqtrd 2861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ∪
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) |
108 | | eqid 2778 |
. . . . . . . 8
⊢ ∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) = ∪
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) |
109 | 108 | cncnpi 21501 |
. . . . . . 7
⊢ (((𝐹 ↾ (0(ball‘(abs
∘ − ))𝑀))
∈ (((TopOpen‘ℂfld) ↾t
(0(ball‘(abs ∘ − ))𝑀)) Cn (TopOpen‘ℂfld))
∧ 𝑎 ∈ ∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀))) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
((((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) |
110 | 102, 107,
109 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
((((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) |
111 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
(TopOpen‘ℂfld) ∈ Top) |
112 | | cnex 10355 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
113 | 112, 11 | ssexi 5042 |
. . . . . . . . . 10
⊢ 𝑆 ∈ V |
114 | 113 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ V) |
115 | | restabs 21388 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆 ∧ 𝑆 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) =
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) |
116 | 111, 70, 114, 115 | syl3anc 1439 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) =
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) |
117 | 116 | oveq1d 6939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))) |
118 | 117 | fveq1d 6450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎) = ((((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) |
119 | 110, 118 | eleqtrrd 2862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) |
120 | | resttop 21383 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
121 | 103, 113,
120 | mp2an 682 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top |
122 | 121 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
123 | | df-ss 3806 |
. . . . . . . . . 10
⊢
((0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆 ↔ ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘
− ))𝑀)) |
124 | 70, 123 | sylib 210 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘
− ))𝑀)) |
125 | 96 | cnfldtopn 23004 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
126 | 125 | blopn 22724 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑀 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑀) ∈
(TopOpen‘ℂfld)) |
127 | 56, 57, 60, 126 | syl3anc 1439 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ∈
(TopOpen‘ℂfld)) |
128 | | elrestr 16486 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V ∧
(0(ball‘(abs ∘ − ))𝑀) ∈
(TopOpen‘ℂfld)) → ((0(ball‘(abs ∘
− ))𝑀) ∩ 𝑆) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
129 | 111, 114,
127, 128 | syl3anc 1439 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
130 | 124, 129 | eqeltrrd 2860 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
131 | | isopn3i 21305 |
. . . . . . . 8
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀)) =
(0(ball‘(abs ∘ − ))𝑀)) |
132 | 121, 130,
131 | sylancr 581 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀)) =
(0(ball‘(abs ∘ − ))𝑀)) |
133 | 63, 132 | eleqtrrd 2862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀))) |
134 | 93 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
135 | 104 | restuni 21385 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
136 | 103, 11, 135 | mp2an 682 |
. . . . . . 7
⊢ 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆) |
137 | 136, 104 | cnprest 21512 |
. . . . . 6
⊢
(((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆) ∧ (𝑎 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀)) ∧
𝐹:𝑆⟶ℂ)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎) ↔ (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎))) |
138 | 122, 70, 133, 134, 137 | syl22anc 829 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎) ↔ (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎))) |
139 | 119, 138 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)) |
140 | 139 | ralrimiva 3148 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)) |
141 | | resttopon 21384 |
. . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
142 | 98, 11, 141 | mp2an 682 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) |
143 | | cncnp 21503 |
. . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)))) |
144 | 142, 98, 143 | mp2an 682 |
. . 3
⊢ (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎))) |
145 | 93, 140, 144 | sylanbrc 578 |
. 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
146 | | eqid 2778 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
147 | 96, 146, 99 | cncfcn 23131 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
148 | 11, 95, 147 | mp2an 682 |
. 2
⊢ (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld)) |
149 | 145, 148 | syl6eleqr 2870 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |