| Step | Hyp | Ref
| Expression |
| 1 | | cnheibor.2 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldtop 24804 |
. . . 4
⊢ 𝐽 ∈ Top |
| 3 | | cnheibor.4 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
| 4 | 3 | cnref1o 13027 |
. . . . . . . . 9
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ |
| 5 | | f1ofn 6849 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ ×
ℝ)) |
| 6 | | elpreima 7078 |
. . . . . . . . 9
⊢ (𝐹 Fn (ℝ × ℝ)
→ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋))) |
| 7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) |
| 8 | | 1st2nd2 8053 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (ℝ ×
ℝ) → 𝑢 =
〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 9 | 8 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 10 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (1st ‘𝑢) ∈ ℝ) |
| 11 | 10 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℝ) |
| 12 | 11 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℂ) |
| 13 | 12 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ∈
ℝ) |
| 14 | 1 | cnfldtopon 24803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 15 | 14 | toponunii 22922 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪ 𝐽 |
| 16 | 15 | cldss 23037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ) |
| 19 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ 𝑋) |
| 20 | 18, 19 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ ℂ) |
| 21 | 20 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ∈ ℝ) |
| 22 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ) |
| 23 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ ×
ℝ)) |
| 24 | | f1ocnvfv1 7296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) →
(◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
| 25 | 4, 23, 24 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
| 26 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹‘𝑢))) |
| 27 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹‘𝑢))) |
| 28 | 26, 27 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐹‘𝑢) → 〈(ℜ‘𝑧), (ℑ‘𝑧)〉 =
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
| 29 | 3 | cnrecnv 15204 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦
〈(ℜ‘𝑧),
(ℑ‘𝑧)〉) |
| 30 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉 ∈ V |
| 31 | 28, 29, 30 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑢) ∈ ℂ → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
| 32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
| 33 | 25, 32 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
| 34 | 33 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (1st
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
| 35 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘(𝐹‘𝑢)) ∈ V |
| 36 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℑ‘(𝐹‘𝑢)) ∈ V |
| 37 | 35, 36 | op1st 8022 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℜ‘(𝐹‘𝑢)) |
| 38 | 34, 37 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (ℜ‘(𝐹‘𝑢))) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) =
(abs‘(ℜ‘(𝐹‘𝑢)))) |
| 40 | | absrele 15347 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
| 41 | 20, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
| 42 | 39, 41 | eqbrtrd 5165 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐹‘𝑢) → (abs‘𝑧) = (abs‘(𝐹‘𝑢))) |
| 44 | 43 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
| 45 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅) |
| 46 | 44, 45, 19 | rspcdva 3623 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ≤ 𝑅) |
| 47 | 13, 21, 22, 42, 46 | letrd 11418 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤ 𝑅) |
| 48 | 11, 22 | absled 15469 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(1st
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅))) |
| 49 | 47, 48 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅)) |
| 50 | 49 | simpld 494 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st ‘𝑢)) |
| 51 | 49 | simprd 495 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ≤ 𝑅) |
| 52 | | renegcl 11572 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ) |
| 53 | 22, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ) |
| 54 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((1st ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((1st
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(1st ‘𝑢)
∧ (1st ‘𝑢) ≤ 𝑅))) |
| 55 | 53, 22, 54 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((1st ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st
‘𝑢) ∧
(1st ‘𝑢)
≤ 𝑅))) |
| 56 | 11, 50, 51, 55 | mpbir3and 1343 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈ (-𝑅[,]𝑅)) |
| 57 | | xp2nd 8047 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (2nd ‘𝑢) ∈ ℝ) |
| 58 | 57 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℝ) |
| 59 | 58 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℂ) |
| 60 | 59 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ∈
ℝ) |
| 61 | 33 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (2nd
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
| 62 | 35, 36 | op2nd 8023 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℑ‘(𝐹‘𝑢)) |
| 63 | 61, 62 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (ℑ‘(𝐹‘𝑢))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) =
(abs‘(ℑ‘(𝐹‘𝑢)))) |
| 65 | | absimle 15348 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
| 66 | 20, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
| 67 | 64, 66 | eqbrtrd 5165 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
| 68 | 60, 21, 22, 67, 46 | letrd 11418 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤ 𝑅) |
| 69 | 58, 22 | absled 15469 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(2nd
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅))) |
| 70 | 68, 69 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅)) |
| 71 | 70 | simpld 494 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd ‘𝑢)) |
| 72 | 70 | simprd 495 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ≤ 𝑅) |
| 73 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((2nd ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((2nd
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(2nd ‘𝑢)
∧ (2nd ‘𝑢) ≤ 𝑅))) |
| 74 | 53, 22, 73 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((2nd ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd
‘𝑢) ∧
(2nd ‘𝑢)
≤ 𝑅))) |
| 75 | 58, 71, 72, 74 | mpbir3and 1343 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈ (-𝑅[,]𝑅)) |
| 76 | 56, 75 | opelxpd 5724 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
| 77 | 9, 76 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
| 78 | 77 | ex 412 |
. . . . . . . 8
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
| 79 | 7, 78 | biimtrid 242 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (◡𝐹 “ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
| 80 | 79 | ssrdv 3989 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
| 81 | | f1ofun 6850 |
. . . . . . . 8
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → Fun 𝐹) |
| 82 | 4, 81 | ax-mp 5 |
. . . . . . 7
⊢ Fun 𝐹 |
| 83 | | f1ofo 6855 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ) |
| 84 | | forn 6823 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–onto→ℂ →
ran 𝐹 =
ℂ) |
| 85 | 4, 83, 84 | mp2b 10 |
. . . . . . . 8
⊢ ran 𝐹 = ℂ |
| 86 | 17, 85 | sseqtrrdi 4025 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹) |
| 87 | | funimass1 6648 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑋 ⊆ ran 𝐹) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
| 88 | 82, 86, 87 | sylancr 587 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
| 89 | 80, 88 | mpd 15 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
| 90 | | cnheibor.5 |
. . . . 5
⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
| 91 | 89, 90 | sseqtrrdi 4025 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ 𝑌) |
| 92 | | eqid 2737 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 93 | 3, 92, 1 | cnrehmeo 24984 |
. . . . . . 7
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) |
| 94 | | imaexg 7935 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V) |
| 95 | 93, 94 | ax-mp 5 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V |
| 96 | 90, 95 | eqeltri 2837 |
. . . . 5
⊢ 𝑌 ∈ V |
| 97 | 96 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V) |
| 98 | | restabs 23173 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
| 99 | 2, 91, 97, 98 | mp3an2i 1468 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
| 100 | | cnheibor.3 |
. . 3
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
| 101 | 99, 100 | eqtr4di 2795 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = 𝑇) |
| 102 | 90 | oveq2i 7442 |
. . . . 5
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
| 103 | | ishmeo 23767 |
. . . . . . . 8
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,)))))) |
| 104 | 93, 103 | mpbi 230 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,))))) |
| 105 | 104 | simpli 483 |
. . . . . 6
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) |
| 106 | | iccssre 13469 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
| 107 | 52, 106 | mpancom 688 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ) |
| 108 | 1, 92 | rerest 24825 |
. . . . . . . . . 10
⊢ ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
| 110 | 109, 109 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
| 111 | | retop 24782 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
| 112 | | ovex 7464 |
. . . . . . . . 9
⊢ (-𝑅[,]𝑅) ∈ V |
| 113 | | txrest 23639 |
. . . . . . . . 9
⊢
((((topGen‘ran (,)) ∈ Top ∧ (topGen‘ran (,)) ∈
Top) ∧ ((-𝑅[,]𝑅) ∈ V ∧ (-𝑅[,]𝑅) ∈ V)) → (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
| 114 | 111, 111,
112, 112, 113 | mp4an 693 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅))) |
| 115 | 110, 114 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
| 116 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) |
| 117 | 92, 116 | icccmp 24847 |
. . . . . . . . . 10
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
| 118 | 52, 117 | mpancom 688 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
| 119 | 109, 118 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) |
| 120 | | txcmp 23651 |
. . . . . . . 8
⊢ (((𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
| 121 | 119, 119,
120 | syl2anc 584 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
| 122 | 115, 121 | eqeltrrd 2842 |
. . . . . 6
⊢ (𝑅 ∈ ℝ →
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) |
| 123 | | imacmp 23405 |
. . . . . 6
⊢ ((𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
| 124 | 105, 122,
123 | sylancr 587 |
. . . . 5
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
| 125 | 102, 124 | eqeltrid 2845 |
. . . 4
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t 𝑌) ∈ Comp) |
| 126 | 125 | ad2antrl 728 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽 ↾t 𝑌) ∈ Comp) |
| 127 | | imassrn 6089 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹 |
| 128 | 90, 127 | eqsstri 4030 |
. . . . 5
⊢ 𝑌 ⊆ ran 𝐹 |
| 129 | | f1of 6848 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ ×
ℝ)⟶ℂ) |
| 130 | | frn 6743 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ) |
| 131 | 4, 129, 130 | mp2b 10 |
. . . . 5
⊢ ran 𝐹 ⊆
ℂ |
| 132 | 128, 131 | sstri 3993 |
. . . 4
⊢ 𝑌 ⊆
ℂ |
| 133 | | simpl 482 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽)) |
| 134 | 15 | restcldi 23181 |
. . . 4
⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋 ⊆ 𝑌) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
| 135 | 132, 133,
91, 134 | mp3an2i 1468 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
| 136 | | cmpcld 23410 |
. . 3
⊢ (((𝐽 ↾t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
| 137 | 126, 135,
136 | syl2anc 584 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
| 138 | 101, 137 | eqeltrrd 2842 |
1
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) |