| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sumex 15725 | . . . . . 6
⊢
Σ𝑗 ∈
ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V | 
| 2 | 1 | rgenw 3064 | . . . . 5
⊢
∀𝑦 ∈
𝑆 Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V | 
| 3 |  | pserf.f | . . . . . 6
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) | 
| 4 | 3 | fnmpt 6707 | . . . . 5
⊢
(∀𝑦 ∈
𝑆 Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ V → 𝐹 Fn 𝑆) | 
| 5 | 2, 4 | mp1i 13 | . . . 4
⊢ (𝜑 → 𝐹 Fn 𝑆) | 
| 6 |  | psercn.s | . . . . . . . . . . 11
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) | 
| 7 |  | cnvimass 6099 | . . . . . . . . . . . 12
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs | 
| 8 |  | absf 15377 | . . . . . . . . . . . . 13
⊢
abs:ℂ⟶ℝ | 
| 9 | 8 | fdmi 6746 | . . . . . . . . . . . 12
⊢ dom abs =
ℂ | 
| 10 | 7, 9 | sseqtri 4031 | . . . . . . . . . . 11
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ | 
| 11 | 6, 10 | eqsstri 4029 | . . . . . . . . . 10
⊢ 𝑆 ⊆
ℂ | 
| 12 | 11 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 13 | 12 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) | 
| 14 |  | 0cn 11254 | . . . . . . . . . . 11
⊢ 0 ∈
ℂ | 
| 15 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 16 | 15 | cnmetdval 24792 | . . . . . . . . . . 11
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) | 
| 17 | 14, 13, 16 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) | 
| 18 |  | abssub 15366 | . . . . . . . . . . 11
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0))) | 
| 19 | 14, 13, 18 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0))) | 
| 20 | 13 | subid1d 11610 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 − 0) = 𝑎) | 
| 21 | 20 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘(𝑎 − 0)) = (abs‘𝑎)) | 
| 22 | 17, 19, 21 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) = (abs‘𝑎)) | 
| 23 |  | breq2 5146 | . . . . . . . . . . 11
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) | 
| 24 |  | breq2 5146 | . . . . . . . . . . 11
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) | 
| 25 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) | 
| 26 | 25, 6 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (◡abs “ (0[,)𝑅))) | 
| 27 |  | ffn 6735 | . . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) | 
| 28 |  | elpreima 7077 | . . . . . . . . . . . . . . . . . 18
⊢ (abs Fn
ℂ → (𝑎 ∈
(◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))) | 
| 29 | 8, 27, 28 | mp2b 10 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) | 
| 30 | 26, 29 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) | 
| 31 | 30 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ (0[,)𝑅)) | 
| 32 |  | 0re 11264 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ | 
| 33 |  | iccssxr 13471 | . . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ⊆ ℝ* | 
| 34 |  | pserf.g | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) | 
| 35 |  | pserf.a | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 36 |  | pserf.r | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 37 | 34, 35, 36 | radcnvcl 26461 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈ (0[,]+∞)) | 
| 39 | 33, 38 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈
ℝ*) | 
| 40 |  | elico2 13452 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑅
∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) | 
| 41 | 32, 39, 40 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) | 
| 42 | 31, 41 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅)) | 
| 43 | 42 | simp3d 1144 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑅) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅) | 
| 45 | 13 | abscld 15476 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) | 
| 46 |  | avglt1 12506 | . . . . . . . . . . . . 13
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) | 
| 47 | 45, 46 | sylan 580 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) | 
| 48 | 44, 47 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)) | 
| 49 | 45 | ltp1d 12199 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1)) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1)) | 
| 51 | 23, 24, 48, 50 | ifbothda 4563 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))) | 
| 52 |  | psercn.m | . . . . . . . . . 10
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) | 
| 53 | 51, 52 | breqtrrdi 5184 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) | 
| 54 | 22, 53 | eqbrtrd 5164 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(abs ∘ − )𝑎) < 𝑀) | 
| 55 |  | cnxmet 24794 | . . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 56 | 34, 3, 35, 36, 6, 52 | psercnlem1 26470 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) | 
| 57 | 56 | simp1d 1142 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) | 
| 58 | 57 | rpxrd 13079 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ*) | 
| 59 |  | elbl 24399 | . . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑀 ∈
ℝ*) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs
∘ − )𝑎) <
𝑀))) | 
| 60 | 55, 14, 58, 59 | mp3an12i 1466 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs
∘ − )𝑎) <
𝑀))) | 
| 61 | 13, 54, 60 | mpbir2and 713 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀)) | 
| 62 | 61 | fvresd 6925 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀))‘𝑎) = (𝐹‘𝑎)) | 
| 63 | 3 | reseq1i 5992 | . . . . . . . . . 10
⊢ (𝐹 ↾ (0(ball‘(abs
∘ − ))𝑀)) =
((𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ −
))𝑀)) | 
| 64 | 34, 3, 35, 36, 6, 56 | psercnlem2 26469 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))𝑀) ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ (◡abs “ (0[,]𝑀)) ∧ (◡abs “ (0[,]𝑀)) ⊆ 𝑆)) | 
| 65 | 64 | simp2d 1143 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆ (◡abs “ (0[,]𝑀))) | 
| 66 | 64 | simp3d 1144 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡abs “ (0[,]𝑀)) ⊆ 𝑆) | 
| 67 | 65, 66 | sstrd 3993 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆ 𝑆) | 
| 68 | 67 | resmptd 6057 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ −
))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗))) | 
| 69 | 63, 68 | eqtrid 2788 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗))) | 
| 70 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ Σ𝑗 ∈
ℕ0 ((𝐺‘𝑦)‘𝑗)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) | 
| 71 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) | 
| 72 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑦 → (𝐺‘𝑘) = (𝐺‘𝑦)) | 
| 73 | 72 | seqeq3d 14051 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑦 → seq0( + , (𝐺‘𝑘)) = seq0( + , (𝐺‘𝑦))) | 
| 74 | 73 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (seq0( + , (𝐺‘𝑘))‘𝑠) = (seq0( + , (𝐺‘𝑦))‘𝑠)) | 
| 75 | 74 | cbvmptv 5254 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ (seq0( + , (𝐺‘𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑠)) | 
| 76 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑖 → (seq0( + , (𝐺‘𝑦))‘𝑠) = (seq0( + , (𝐺‘𝑦))‘𝑖)) | 
| 77 | 76 | mpteq2dv 5243 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑖 → (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑖))) | 
| 78 | 75, 77 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑖 → (𝑘 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ (seq0( + ,
(𝐺‘𝑦))‘𝑖))) | 
| 79 | 78 | cbvmptv 5254 | . . . . . . . . . 10
⊢ (𝑠 ∈ ℕ0
↦ (𝑘 ∈
(0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺‘𝑘))‘𝑠))) = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ (0(ball‘(abs
∘ − ))𝑀)
↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) | 
| 80 | 57 | rpred 13078 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) | 
| 81 | 56 | simp3d 1144 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) | 
| 82 | 34, 70, 71, 36, 79, 80, 81, 65 | psercn2 26467 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑦 ∈ (0(ball‘(abs ∘ −
))𝑀) ↦ Σ𝑗 ∈ ℕ0
((𝐺‘𝑦)‘𝑗)) ∈ ((0(ball‘(abs ∘ −
))𝑀)–cn→ℂ)) | 
| 83 | 69, 82 | eqeltrd 2840 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ)) | 
| 84 |  | cncff 24920 | . . . . . . . 8
⊢ ((𝐹 ↾ (0(ball‘(abs
∘ − ))𝑀))
∈ ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)):(0(ball‘(abs
∘ − ))𝑀)⟶ℂ) | 
| 85 | 83, 84 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)):(0(ball‘(abs
∘ − ))𝑀)⟶ℂ) | 
| 86 | 85, 61 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀))‘𝑎) ∈
ℂ) | 
| 87 | 62, 86 | eqeltrrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹‘𝑎) ∈ ℂ) | 
| 88 | 87 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (𝐹‘𝑎) ∈ ℂ) | 
| 89 |  | ffnfv 7138 | . . . 4
⊢ (𝐹:𝑆⟶ℂ ↔ (𝐹 Fn 𝑆 ∧ ∀𝑎 ∈ 𝑆 (𝐹‘𝑎) ∈ ℂ)) | 
| 90 | 5, 88, 89 | sylanbrc 583 | . . 3
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | 
| 91 | 67, 11 | sstrdi 3995 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ⊆
ℂ) | 
| 92 |  | ssid 4005 | . . . . . . . . 9
⊢ ℂ
⊆ ℂ | 
| 93 |  | eqid 2736 | . . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 94 |  | eqid 2736 | . . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t
(0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) | 
| 95 | 93 | cnfldtopon 24804 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 96 | 95 | toponrestid 22928 | . . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 97 | 93, 94, 96 | cncfcn 24937 | . . . . . . . . 9
⊢
(((0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) | 
| 98 | 91, 92, 97 | sylancl 586 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) | 
| 99 | 83, 98 | eleqtrd 2842 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) Cn
(TopOpen‘ℂfld))) | 
| 100 | 93 | cnfldtop 24805 | . . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 101 |  | unicntop 24807 | . . . . . . . . . 10
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 102 | 101 | restuni 23171 | . . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ) → (0(ball‘(abs
∘ − ))𝑀) =
∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀))) | 
| 103 | 100, 91, 102 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) = ∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀))) | 
| 104 | 61, 103 | eleqtrd 2842 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ∪
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) | 
| 105 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ ((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) = ∪
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) | 
| 106 | 105 | cncnpi 23287 | . . . . . . 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))‘𝑎)) | 
| 107 | 99, 104, 106 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
((((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) | 
| 108 |  | cnex 11237 | . . . . . . . . . . 11
⊢ ℂ
∈ V | 
| 109 | 108, 11 | ssexi 5321 | . . . . . . . . . 10
⊢ 𝑆 ∈ V | 
| 110 | 109 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ V) | 
| 111 |  | restabs 23174 | . . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆 ∧ 𝑆 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) =
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) | 
| 112 | 100, 67, 110, 111 | mp3an2i 1467 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) =
((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀))) | 
| 113 | 112 | oveq1d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))) | 
| 114 | 113 | fveq1d 6907 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎) = ((((TopOpen‘ℂfld)
↾t (0(ball‘(abs ∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) | 
| 115 | 107, 114 | eleqtrrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎)) | 
| 116 |  | resttop 23169 | . . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) | 
| 117 | 100, 109,
116 | mp2an 692 | . . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top | 
| 118 | 117 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) | 
| 119 |  | dfss2 3968 | . . . . . . . . . 10
⊢
((0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆 ↔ ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘
− ))𝑀)) | 
| 120 | 67, 119 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘
− ))𝑀)) | 
| 121 | 93 | cnfldtopn 24803 | . . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) | 
| 122 | 121 | blopn 24514 | . . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑀 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑀) ∈
(TopOpen‘ℂfld)) | 
| 123 | 55, 14, 58, 122 | mp3an12i 1466 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ∈
(TopOpen‘ℂfld)) | 
| 124 |  | elrestr 17474 | . . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V ∧
(0(ball‘(abs ∘ − ))𝑀) ∈
(TopOpen‘ℂfld)) → ((0(ball‘(abs ∘
− ))𝑀) ∩ 𝑆) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 125 | 100, 109,
123, 124 | mp3an12i 1466 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((0(ball‘(abs ∘ −
))𝑀) ∩ 𝑆) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 126 | 120, 125 | eqeltrrd 2841 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))𝑀) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 127 |  | isopn3i 23091 | . . . . . . . 8
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧
(0(ball‘(abs ∘ − ))𝑀) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀)) =
(0(ball‘(abs ∘ − ))𝑀)) | 
| 128 | 117, 126,
127 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀)) =
(0(ball‘(abs ∘ − ))𝑀)) | 
| 129 | 61, 128 | eleqtrrd 2843 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs
∘ − ))𝑀))) | 
| 130 | 90 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) | 
| 131 | 101 | restuni 23171 | . . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 132 | 100, 11, 131 | mp2an 692 | . . . . . . 7
⊢ 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆) | 
| 133 | 132, 101 | cnprest 23298 | . . . . . 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))‘𝑎))) | 
| 134 | 118, 67, 129, 130, 133 | syl22anc 838 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎) ↔ (𝐹 ↾ (0(ball‘(abs ∘ −
))𝑀)) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs
∘ − ))𝑀)) CnP
(TopOpen‘ℂfld))‘𝑎))) | 
| 135 | 115, 134 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)) | 
| 136 | 135 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)) | 
| 137 |  | resttopon 23170 | . . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) | 
| 138 | 95, 11, 137 | mp2an 692 | . . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) | 
| 139 |  | cncnp 23289 | . . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎)))) | 
| 140 | 138, 95, 139 | mp2an 692 | . . 3
⊢ (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑎))) | 
| 141 | 90, 136, 140 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) | 
| 142 |  | eqid 2736 | . . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) | 
| 143 | 93, 142, 96 | cncfcn 24937 | . . 3
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) | 
| 144 | 11, 92, 143 | mp2an 692 | . 2
⊢ (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld)) | 
| 145 | 141, 144 | eleqtrrdi 2851 | 1
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |