Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtop 22397 |
. . . 4
⊢ 𝐽 ∈ Top |
3 | | cnheibor.4 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
4 | 3 | cnref1o 11703 |
. . . . . . . . 9
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ |
5 | | f1ofn 6051 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ ×
ℝ)) |
6 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐹 Fn (ℝ × ℝ)
→ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋))) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) |
8 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (ℝ ×
ℝ) → 𝑢 =
〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
9 | 8 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
10 | | xp1st 7089 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (1st ‘𝑢) ∈ ℝ) |
11 | 10 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℝ) |
12 | 11 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℂ) |
13 | 12 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ∈
ℝ) |
14 | 1 | cnfldtopon 22396 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐽 ∈
(TopOn‘ℂ) |
15 | 14 | toponunii 20547 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪ 𝐽 |
16 | 15 | cldss 20643 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ) |
19 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ 𝑋) |
20 | 18, 19 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ ℂ) |
21 | 20 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ∈ ℝ) |
22 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ) |
23 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ ×
ℝ)) |
24 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) →
(◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
25 | 4, 23, 24 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹‘𝑢))) |
27 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹‘𝑢))) |
28 | 26, 27 | opeq12d 4348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐹‘𝑢) → 〈(ℜ‘𝑧), (ℑ‘𝑧)〉 =
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
29 | 3 | cnrecnv 13753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦
〈(ℜ‘𝑧),
(ℑ‘𝑧)〉) |
30 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉 ∈ V |
31 | 28, 29, 30 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑢) ∈ ℂ → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
33 | 25, 32 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
34 | 33 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (1st
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
35 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘(𝐹‘𝑢)) ∈ V |
36 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℑ‘(𝐹‘𝑢)) ∈ V |
37 | 35, 36 | op1st 7067 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℜ‘(𝐹‘𝑢)) |
38 | 34, 37 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (ℜ‘(𝐹‘𝑢))) |
39 | 38 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) =
(abs‘(ℜ‘(𝐹‘𝑢)))) |
40 | | absrele 13896 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
41 | 20, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
42 | 39, 41 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
43 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝐹‘𝑢) → (abs‘𝑧) = (abs‘(𝐹‘𝑢))) |
45 | 44 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐹‘𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
46 | 45 | rspcv 3278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑢) ∈ 𝑋 → (∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅 → (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
47 | 19, 43, 46 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ≤ 𝑅) |
48 | 13, 21, 22, 42, 47 | letrd 10073 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤ 𝑅) |
49 | 11, 22 | absled 14017 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(1st
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅))) |
50 | 48, 49 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅)) |
51 | 50 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st ‘𝑢)) |
52 | 50 | simprd 478 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ≤ 𝑅) |
53 | | renegcl 10223 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ) |
54 | 22, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ) |
55 | | elicc2 12109 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((1st ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((1st
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(1st ‘𝑢)
∧ (1st ‘𝑢) ≤ 𝑅))) |
56 | 54, 22, 55 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((1st ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st
‘𝑢) ∧
(1st ‘𝑢)
≤ 𝑅))) |
57 | 11, 51, 52, 56 | mpbir3and 1238 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈ (-𝑅[,]𝑅)) |
58 | | xp2nd 7090 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (2nd ‘𝑢) ∈ ℝ) |
59 | 58 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℝ) |
60 | 59 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℂ) |
61 | 60 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ∈
ℝ) |
62 | 33 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (2nd
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
63 | 35, 36 | op2nd 7068 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℑ‘(𝐹‘𝑢)) |
64 | 62, 63 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (ℑ‘(𝐹‘𝑢))) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) =
(abs‘(ℑ‘(𝐹‘𝑢)))) |
66 | | absimle 13897 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
67 | 20, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
68 | 65, 67 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
69 | 61, 21, 22, 68, 47 | letrd 10073 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤ 𝑅) |
70 | 59, 22 | absled 14017 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(2nd
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅))) |
71 | 69, 70 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅)) |
72 | 71 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd ‘𝑢)) |
73 | 71 | simprd 478 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ≤ 𝑅) |
74 | | elicc2 12109 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((2nd ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((2nd
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(2nd ‘𝑢)
∧ (2nd ‘𝑢) ≤ 𝑅))) |
75 | 54, 22, 74 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((2nd ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd
‘𝑢) ∧
(2nd ‘𝑢)
≤ 𝑅))) |
76 | 59, 72, 73, 75 | mpbir3and 1238 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈ (-𝑅[,]𝑅)) |
77 | 57, 76 | opelxpd 5073 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
78 | 9, 77 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
79 | 78 | ex 449 |
. . . . . . . 8
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
80 | 7, 79 | syl5bi 231 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (◡𝐹 “ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
81 | 80 | ssrdv 3574 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
82 | | f1ofun 6052 |
. . . . . . . 8
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → Fun 𝐹) |
83 | 4, 82 | ax-mp 5 |
. . . . . . 7
⊢ Fun 𝐹 |
84 | | f1ofo 6057 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ) |
85 | | forn 6031 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–onto→ℂ →
ran 𝐹 =
ℂ) |
86 | 4, 84, 85 | mp2b 10 |
. . . . . . . 8
⊢ ran 𝐹 = ℂ |
87 | 17, 86 | syl6sseqr 3615 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹) |
88 | | funimass1 5885 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑋 ⊆ ran 𝐹) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
89 | 83, 87, 88 | sylancr 694 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
90 | 81, 89 | mpd 15 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
91 | | cnheibor.5 |
. . . . 5
⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
92 | 90, 91 | syl6sseqr 3615 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ 𝑌) |
93 | | eqid 2610 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
94 | 3, 93, 1 | cnrehmeo 22560 |
. . . . . . 7
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) |
95 | | imaexg 6995 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V) |
96 | 94, 95 | ax-mp 5 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V |
97 | 91, 96 | eqeltri 2684 |
. . . . 5
⊢ 𝑌 ∈ V |
98 | 97 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V) |
99 | | restabs 20779 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
100 | 2, 92, 98, 99 | mp3an2i 1421 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
101 | | cnheibor.3 |
. . 3
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
102 | 100, 101 | syl6eqr 2662 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = 𝑇) |
103 | 91 | oveq2i 6560 |
. . . . 5
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
104 | | ishmeo 21372 |
. . . . . . . 8
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,)))))) |
105 | 94, 104 | mpbi 219 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,))))) |
106 | 105 | simpli 473 |
. . . . . 6
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) |
107 | | iccssre 12126 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
108 | 53, 107 | mpancom 700 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ) |
109 | 1, 93 | rerest 22415 |
. . . . . . . . . 10
⊢ ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
110 | 108, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
111 | 110, 110 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
112 | | retop 22375 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
113 | | ovex 6577 |
. . . . . . . . 9
⊢ (-𝑅[,]𝑅) ∈ V |
114 | | txrest 21244 |
. . . . . . . . 9
⊢
((((topGen‘ran (,)) ∈ Top ∧ (topGen‘ran (,)) ∈
Top) ∧ ((-𝑅[,]𝑅) ∈ V ∧ (-𝑅[,]𝑅) ∈ V)) → (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
115 | 112, 112,
113, 113, 114 | mp4an 705 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅))) |
116 | 111, 115 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
117 | | eqid 2610 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) |
118 | 93, 117 | icccmp 22436 |
. . . . . . . . . 10
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
119 | 53, 118 | mpancom 700 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
120 | 110, 119 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) |
121 | | txcmp 21256 |
. . . . . . . 8
⊢ (((𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
122 | 120, 120,
121 | syl2anc 691 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
123 | 116, 122 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝑅 ∈ ℝ →
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) |
124 | | imacmp 21010 |
. . . . . 6
⊢ ((𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
125 | 106, 123,
124 | sylancr 694 |
. . . . 5
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
126 | 103, 125 | syl5eqel 2692 |
. . . 4
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t 𝑌) ∈ Comp) |
127 | 126 | ad2antrl 760 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽 ↾t 𝑌) ∈ Comp) |
128 | | imassrn 5396 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹 |
129 | 91, 128 | eqsstri 3598 |
. . . . 5
⊢ 𝑌 ⊆ ran 𝐹 |
130 | | f1of 6050 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ ×
ℝ)⟶ℂ) |
131 | | frn 5966 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ) |
132 | 4, 130, 131 | mp2b 10 |
. . . . 5
⊢ ran 𝐹 ⊆
ℂ |
133 | 129, 132 | sstri 3577 |
. . . 4
⊢ 𝑌 ⊆
ℂ |
134 | | simpl 472 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽)) |
135 | 15 | restcldi 20787 |
. . . 4
⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋 ⊆ 𝑌) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
136 | 133, 134,
92, 135 | mp3an2i 1421 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
137 | | cmpcld 21015 |
. . 3
⊢ (((𝐽 ↾t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
138 | 127, 136,
137 | syl2anc 691 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
139 | 102, 138 | eqeltrrd 2689 |
1
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) |