Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtop 22999 |
. . . 4
⊢ 𝐽 ∈ Top |
3 | | cnheibor.4 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
4 | 3 | cnref1o 12136 |
. . . . . . . . 9
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ |
5 | | f1ofn 6394 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ ×
ℝ)) |
6 | | elpreima 6602 |
. . . . . . . . 9
⊢ (𝐹 Fn (ℝ × ℝ)
→ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋))) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢 ∈ (◡𝐹 “ 𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) |
8 | | 1st2nd2 7486 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (ℝ ×
ℝ) → 𝑢 =
〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
9 | 8 | ad2antrl 718 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
10 | | xp1st 7479 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (1st ‘𝑢) ∈ ℝ) |
11 | 10 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℝ) |
12 | 11 | recnd 10407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈
ℂ) |
13 | 12 | abscld 14587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ∈
ℝ) |
14 | 1 | cnfldtopon 22998 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐽 ∈
(TopOn‘ℂ) |
15 | 14 | toponunii 21132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪ 𝐽 |
16 | 15 | cldss 21245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ) |
17 | 16 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ) |
18 | 17 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ) |
19 | | simprr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ 𝑋) |
20 | 18, 19 | sseldd 3822 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (𝐹‘𝑢) ∈ ℂ) |
21 | 20 | abscld 14587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ∈ ℝ) |
22 | | simplrl 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ) |
23 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ ×
ℝ)) |
24 | | f1ocnvfv1 6806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) →
(◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
25 | 4, 23, 24 | sylancr 581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 𝑢) |
26 | | fveq2 6448 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹‘𝑢))) |
27 | | fveq2 6448 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝐹‘𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹‘𝑢))) |
28 | 26, 27 | opeq12d 4646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐹‘𝑢) → 〈(ℜ‘𝑧), (ℑ‘𝑧)〉 =
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
29 | 3 | cnrecnv 14316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦
〈(ℜ‘𝑧),
(ℑ‘𝑧)〉) |
30 | | opex 5166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉 ∈ V |
31 | 28, 29, 30 | fvmpt 6544 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑢) ∈ ℂ → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (◡𝐹‘(𝐹‘𝑢)) = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
33 | 25, 32 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 = 〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) |
34 | 33 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (1st
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
35 | | fvex 6461 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘(𝐹‘𝑢)) ∈ V |
36 | | fvex 6461 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℑ‘(𝐹‘𝑢)) ∈ V |
37 | 35, 36 | op1st 7455 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℜ‘(𝐹‘𝑢)) |
38 | 34, 37 | syl6eq 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) = (ℜ‘(𝐹‘𝑢))) |
39 | 38 | fveq2d 6452 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) =
(abs‘(ℜ‘(𝐹‘𝑢)))) |
40 | | absrele 14459 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
41 | 20, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
42 | 39, 41 | eqbrtrd 4910 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
43 | | fveq2 6448 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐹‘𝑢) → (abs‘𝑧) = (abs‘(𝐹‘𝑢))) |
44 | 43 | breq1d 4898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹‘𝑢)) ≤ 𝑅)) |
45 | | simplrr 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅) |
46 | 44, 45, 19 | rspcdva 3517 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(𝐹‘𝑢)) ≤ 𝑅) |
47 | 13, 21, 22, 42, 46 | letrd 10535 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(1st
‘𝑢)) ≤ 𝑅) |
48 | 11, 22 | absled 14581 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(1st
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅))) |
49 | 47, 48 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st ‘𝑢) ∧ (1st
‘𝑢) ≤ 𝑅)) |
50 | 49 | simpld 490 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st ‘𝑢)) |
51 | 49 | simprd 491 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ≤ 𝑅) |
52 | | renegcl 10688 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ) |
53 | 22, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ) |
54 | | elicc2 12554 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((1st ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((1st
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(1st ‘𝑢)
∧ (1st ‘𝑢) ≤ 𝑅))) |
55 | 53, 22, 54 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((1st ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st
‘𝑢) ∧
(1st ‘𝑢)
≤ 𝑅))) |
56 | 11, 50, 51, 55 | mpbir3and 1399 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (1st ‘𝑢) ∈ (-𝑅[,]𝑅)) |
57 | | xp2nd 7480 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (ℝ ×
ℝ) → (2nd ‘𝑢) ∈ ℝ) |
58 | 57 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℝ) |
59 | 58 | recnd 10407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈
ℂ) |
60 | 59 | abscld 14587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ∈
ℝ) |
61 | 33 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (2nd
‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉)) |
62 | 35, 36 | op2nd 7456 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈(ℜ‘(𝐹‘𝑢)), (ℑ‘(𝐹‘𝑢))〉) = (ℑ‘(𝐹‘𝑢)) |
63 | 61, 62 | syl6eq 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) = (ℑ‘(𝐹‘𝑢))) |
64 | 63 | fveq2d 6452 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) =
(abs‘(ℑ‘(𝐹‘𝑢)))) |
65 | | absimle 14460 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ∈ ℂ →
(abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
66 | 20, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹‘𝑢))) ≤ (abs‘(𝐹‘𝑢))) |
67 | 64, 66 | eqbrtrd 4910 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤
(abs‘(𝐹‘𝑢))) |
68 | 60, 21, 22, 67, 46 | letrd 10535 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (abs‘(2nd
‘𝑢)) ≤ 𝑅) |
69 | 58, 22 | absled 14581 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((abs‘(2nd
‘𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅))) |
70 | 68, 69 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd ‘𝑢) ∧ (2nd
‘𝑢) ≤ 𝑅)) |
71 | 70 | simpld 490 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd ‘𝑢)) |
72 | 70 | simprd 491 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ≤ 𝑅) |
73 | | elicc2 12554 |
. . . . . . . . . . . . 13
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((2nd ‘𝑢)
∈ (-𝑅[,]𝑅) ↔ ((2nd
‘𝑢) ∈ ℝ
∧ -𝑅 ≤
(2nd ‘𝑢)
∧ (2nd ‘𝑢) ≤ 𝑅))) |
74 | 53, 22, 73 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → ((2nd ‘𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd ‘𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd
‘𝑢) ∧
(2nd ‘𝑢)
≤ 𝑅))) |
75 | 58, 71, 72, 74 | mpbir3and 1399 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → (2nd ‘𝑢) ∈ (-𝑅[,]𝑅)) |
76 | 56, 75 | opelxpd 5395 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
77 | 9, 76 | eqeltrd 2859 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
78 | 77 | ex 403 |
. . . . . . . 8
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧
(𝐹‘𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
79 | 7, 78 | syl5bi 234 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (◡𝐹 “ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
80 | 79 | ssrdv 3827 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
81 | | f1ofun 6395 |
. . . . . . . 8
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → Fun 𝐹) |
82 | 4, 81 | ax-mp 5 |
. . . . . . 7
⊢ Fun 𝐹 |
83 | | f1ofo 6400 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ) |
84 | | forn 6371 |
. . . . . . . . 9
⊢ (𝐹:(ℝ ×
ℝ)–onto→ℂ →
ran 𝐹 =
ℂ) |
85 | 4, 83, 84 | mp2b 10 |
. . . . . . . 8
⊢ ran 𝐹 = ℂ |
86 | 17, 85 | syl6sseqr 3871 |
. . . . . . 7
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹) |
87 | | funimass1 6218 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑋 ⊆ ran 𝐹) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
88 | 82, 86, 87 | sylancr 581 |
. . . . . 6
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((◡𝐹 “ 𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))) |
89 | 80, 88 | mpd 15 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
90 | | cnheibor.5 |
. . . . 5
⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) |
91 | 89, 90 | syl6sseqr 3871 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ 𝑌) |
92 | | eqid 2778 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
93 | 3, 92, 1 | cnrehmeo 23164 |
. . . . . . 7
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) |
94 | | imaexg 7384 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V) |
95 | 93, 94 | ax-mp 5 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V |
96 | 90, 95 | eqeltri 2855 |
. . . . 5
⊢ 𝑌 ∈ V |
97 | 96 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V) |
98 | | restabs 21381 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
99 | 2, 91, 97, 98 | mp3an2i 1539 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
100 | | cnheibor.3 |
. . 3
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
101 | 99, 100 | syl6eqr 2832 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) = 𝑇) |
102 | 90 | oveq2i 6935 |
. . . . 5
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
103 | | ishmeo 21975 |
. . . . . . . 8
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,)))))) |
104 | 93, 103 | mpbi 222 |
. . . . . . 7
⊢ (𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn ((topGen‘ran (,))
×t (topGen‘ran (,))))) |
105 | 104 | simpli 478 |
. . . . . 6
⊢ 𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) |
106 | | iccssre 12571 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
107 | 52, 106 | mpancom 678 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ) |
108 | 1, 92 | rerest 23019 |
. . . . . . . . . 10
⊢ ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅))) |
110 | 109, 109 | oveq12d 6942 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅)))) |
111 | | retop 22977 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
112 | | ovex 6956 |
. . . . . . . . 9
⊢ (-𝑅[,]𝑅) ∈ V |
113 | | txrest 21847 |
. . . . . . . . 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 683 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran
(,)) ↾t (-𝑅[,]𝑅))) |
115 | 110, 114 | syl6eqr 2832 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) = (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) |
116 | | eqid 2778 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,))
↾t (-𝑅[,]𝑅)) |
117 | 92, 116 | icccmp 23040 |
. . . . . . . . . 10
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
118 | 52, 117 | mpancom 678 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ →
((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp) |
119 | 109, 118 | eqeltrd 2859 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) |
120 | | txcmp 21859 |
. . . . . . . 8
⊢ (((𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽 ↾t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
121 | 119, 119,
120 | syl2anc 579 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ → ((𝐽 ↾t (-𝑅[,]𝑅)) ×t (𝐽 ↾t (-𝑅[,]𝑅))) ∈ Comp) |
122 | 115, 121 | eqeltrrd 2860 |
. . . . . 6
⊢ (𝑅 ∈ ℝ →
(((topGen‘ran (,)) ×t (topGen‘ran (,)))
↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) |
123 | | imacmp 21613 |
. . . . . 6
⊢ ((𝐹 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,))
×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
124 | 105, 122,
123 | sylancr 581 |
. . . . 5
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp) |
125 | 102, 124 | syl5eqel 2863 |
. . . 4
⊢ (𝑅 ∈ ℝ → (𝐽 ↾t 𝑌) ∈ Comp) |
126 | 125 | ad2antrl 718 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽 ↾t 𝑌) ∈ Comp) |
127 | | imassrn 5733 |
. . . . . 6
⊢ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹 |
128 | 90, 127 | eqsstri 3854 |
. . . . 5
⊢ 𝑌 ⊆ ran 𝐹 |
129 | | f1of 6393 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐹:(ℝ ×
ℝ)⟶ℂ) |
130 | | frn 6299 |
. . . . . 6
⊢ (𝐹:(ℝ ×
ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ) |
131 | 4, 129, 130 | mp2b 10 |
. . . . 5
⊢ ran 𝐹 ⊆
ℂ |
132 | 128, 131 | sstri 3830 |
. . . 4
⊢ 𝑌 ⊆
ℂ |
133 | | simpl 476 |
. . . 4
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽)) |
134 | 15 | restcldi 21389 |
. . . 4
⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋 ⊆ 𝑌) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
135 | 132, 133,
91, 134 | mp3an2i 1539 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
136 | | cmpcld 21618 |
. . 3
⊢ (((𝐽 ↾t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽 ↾t 𝑌))) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
137 | 126, 135,
136 | syl2anc 579 |
. 2
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽 ↾t 𝑌) ↾t 𝑋) ∈ Comp) |
138 | 101, 137 | eqeltrrd 2860 |
1
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) |