Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtop 22587 |
. . . 4
⊢ 𝐽 ∈ Top |
3 | | cnheibor.4 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
4 | 3 | cnref1o 11827 |
. . . . . . . . 9
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ |
5 | | f1ofn 6138 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ ×
ℝ)) |
6 | | elpreima 6337 |
. . . . . . . . 9
⊢ (𝐹 Fn (ℝ × ℝ)
→ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋))) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) |
8 | | 1st2nd2 7205 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (ℝ ×
ℝ) → 𝑢 =
〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
9 | 8 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
10 | | xp1st 7198 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (1st ‘𝑢) ∈ ℝ) |
11 | 10 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℝ) |
12 | 11 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℂ) |
13 | 12 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ∈
ℝ) |
14 | 1 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐽 ∈
(TopOn‘ℂ) |
15 | 14 | toponunii 20721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪ 𝐽 |
16 | 15 | cldss 20833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ) |
19 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ 𝑋) |
20 | 18, 19 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ ℂ) |
21 | 20 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ∈ ℝ) |
22 | | simplrl 800 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ) |
23 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ ×
ℝ)) |
24 | | f1ocnvfv1 6532 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) →
(◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
25 | 4, 23, 24 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
26 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹‘𝑢))) |
27 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹‘𝑢))) |
28 | 26, 27 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐹‘𝑢) → 〈(ℜ‘𝑧), (ℑ‘𝑧)〉 =
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
29 | 3 | cnrecnv 13905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦
〈(ℜ‘𝑧),
(ℑ‘𝑧)〉) |
30 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉 ∈ V |
31 | 28, 29, 30 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑢) ∈ ℂ → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
33 | 25, 32 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
34 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (1st
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
35 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘(𝐹‘𝑢)) ∈ V |
36 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℑ‘(𝐹‘𝑢)) ∈ V |
37 | 35, 36 | op1st 7176 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℜ‘(𝐹‘𝑢)) |
38 | 34, 37 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (ℜ‘(𝐹‘𝑢))) |
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) =
(abs‘(ℜ‘(𝐹‘𝑢)))) |
40 | | absrele 14048 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
41 | 20, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
42 | 39, 41 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
43 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅) |
44 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝐹‘𝑢) → (abs‘𝑧) = (abs‘(𝐹‘𝑢))) |
45 | 44 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐹‘𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
46 | 45 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑢) ∈ 𝑋 → (∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅 → (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
47 | 19, 43, 46 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ≤ 𝑅) |
48 | 13, 21, 22, 42, 47 | letrd 10194 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤ 𝑅) |
49 | 11, 22 | absled 14169 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(1st
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅))) |
50 | 48, 49 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅)) |
51 | 50 | simpld 475 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st ‘𝑢)) |
52 | 50 | simprd 479 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ≤ 𝑅) |
53 | | renegcl 10344 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ) |
54 | 22, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ) |
55 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((1st ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((1st
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(1st ‘𝑢)
∧ (1st ‘𝑢) ≤ 𝑅))) |
56 | 54, 22, 55 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((1st ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st
‘𝑢) ∧
(1st ‘𝑢)
≤ 𝑅))) |
57 | 11, 51, 52, 56 | mpbir3and 1245 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈ (-𝑅[,]𝑅)) |
58 | | xp2nd 7199 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (2nd ‘𝑢) ∈ ℝ) |
59 | 58 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℝ) |
60 | 59 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℂ) |
61 | 60 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ∈
ℝ) |
62 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (2nd
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
63 | 35, 36 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℑ‘(𝐹‘𝑢)) |
64 | 62, 63 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (ℑ‘(𝐹‘𝑢))) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) =
(abs‘(ℑ‘(𝐹‘𝑢)))) |
66 | | absimle 14049 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
67 | 20, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
68 | 65, 67 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
69 | 61, 21, 22, 68, 47 | letrd 10194 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤ 𝑅) |
70 | 59, 22 | absled 14169 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(2nd
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅))) |
71 | 69, 70 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅)) |
72 | 71 | simpld 475 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd ‘𝑢)) |
73 | 71 | simprd 479 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ≤ 𝑅) |
74 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((2nd ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((2nd
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(2nd ‘𝑢)
∧ (2nd ‘𝑢) ≤ 𝑅))) |
75 | 54, 22, 74 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((2nd ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd
‘𝑢) ∧
(2nd ‘𝑢)
≤ 𝑅))) |
76 | 59, 72, 73, 75 | mpbir3and 1245 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈ (-𝑅[,]𝑅)) |
77 | 57, 76 | opelxpd 5149 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
78 | 9, 77 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
79 | 78 | ex 450 |
. . . . . . . 8
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
80 | 7, 79 | syl5bi 232 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (◡𝐹 “ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
81 | 80 | ssrdv 3609 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
82 | | f1ofun 6139 |
. . . . . . . 8
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → Fun 𝐹) |
83 | 4, 82 | ax-mp 5 |
. . . . . . 7
⊢ Fun 𝐹 |
84 | | f1ofo 6144 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ) |
85 | | forn 6118 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–onto→ℂ →
ran 𝐹 =
ℂ) |
86 | 4, 84, 85 | mp2b 10 |
. . . . . . . 8
⊢ ran 𝐹 = ℂ |
87 | 17, 86 | syl6sseqr 3652 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹) |
88 | | funimass1 5971 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑋 ⊆ ran 𝐹) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
89 | 83, 87, 88 | sylancr 695 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
90 | 81, 89 | mpd 15 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
91 | | cnheibor.5 |
. . . . 5
⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
92 | 90, 91 | syl6sseqr 3652 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ 𝑌) |
93 | | eqid 2622 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
94 | 3, 93, 1 | cnrehmeo 22752 |
. . . . . . 7
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) |
95 | | imaexg 7103 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V) |
96 | 94, 95 | ax-mp 5 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V |
97 | 91, 96 | eqeltri 2697 |
. . . . 5
⊢ 𝑌 ∈ V |
98 | 97 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V) |
99 | | restabs 20969 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
100 | 2, 92, 98, 99 | mp3an2i 1429 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
101 | | cnheibor.3 |
. . 3
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
102 | 100, 101 | syl6eqr 2674 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = 𝑇) |
103 | 91 | oveq2i 6661 |
. . . . 5
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
104 | | ishmeo 21562 |
. . . . . . . 8
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,)))))) |
105 | 94, 104 | mpbi 220 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,))))) |
106 | 105 | simpli 474 |
. . . . . 6
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) |
107 | | iccssre 12255 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
108 | 53, 107 | mpancom 703 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ) |
109 | 1, 93 | rerest 22607 |
. . . . . . . . . 10
⊢ ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
110 | 108, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
111 | 110, 110 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
112 | | retop 22565 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
113 | | ovex 6678 |
. . . . . . . . 9
⊢ (-𝑅[,]𝑅) ∈ V |
114 | | txrest 21434 |
. . . . . . . . 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 709 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅))) |
116 | 111, 115 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
117 | | eqid 2622 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) |
118 | 93, 117 | icccmp 22628 |
. . . . . . . . . 10
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
119 | 53, 118 | mpancom 703 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
120 | 110, 119 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) |
121 | | txcmp 21446 |
. . . . . . . 8
⊢ (((𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
122 | 120, 120,
121 | syl2anc 693 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
123 | 116, 122 | eqeltrrd 2702 |
. . . . . 6
⊢ (𝑅 ∈ ℝ →
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) |
124 | | imacmp 21200 |
. . . . . 6
⊢ ((𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
125 | 106, 123,
124 | sylancr 695 |
. . . . 5
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
126 | 103, 125 | syl5eqel 2705 |
. . . 4
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t 𝑌) ∈ Comp) |
127 | 126 | ad2antrl 764 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽 ↾t 𝑌) ∈ Comp) |
128 | | imassrn 5477 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹 |
129 | 91, 128 | eqsstri 3635 |
. . . . 5
⊢ 𝑌 ⊆ ran 𝐹 |
130 | | f1of 6137 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ ×
ℝ)⟶ℂ) |
131 | | frn 6053 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ) |
132 | 4, 130, 131 | mp2b 10 |
. . . . 5
⊢ ran 𝐹 ⊆
ℂ |
133 | 129, 132 | sstri 3612 |
. . . 4
⊢ 𝑌 ⊆
ℂ |
134 | | simpl 473 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽)) |
135 | 15 | restcldi 20977 |
. . . 4
⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋 ⊆ 𝑌) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
136 | 133, 134,
92, 135 | mp3an2i 1429 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
137 | | cmpcld 21205 |
. . 3
⊢ (((𝐽 ↾t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
138 | 127, 136,
137 | syl2anc 693 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
139 | 102, 138 | eqeltrrd 2702 |
1
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) |