Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12151 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
2 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
3 | 1, 2 | sstri 3577 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℂ |
4 | 3 | sseli 3564 |
. . . . 5
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
5 | | cxpcn3.d |
. . . . . . 7
⊢ 𝐷 = (◡ℜ “
ℝ+) |
6 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡ℜ “ ℝ+) ⊆
dom ℜ |
7 | | ref 13700 |
. . . . . . . . 9
⊢
ℜ:ℂ⟶ℝ |
8 | 7 | fdmi 5965 |
. . . . . . . 8
⊢ dom
ℜ = ℂ |
9 | 6, 8 | sseqtri 3600 |
. . . . . . 7
⊢ (◡ℜ “ ℝ+) ⊆
ℂ |
10 | 5, 9 | eqsstri 3598 |
. . . . . 6
⊢ 𝐷 ⊆
ℂ |
11 | 10 | sseli 3564 |
. . . . 5
⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ) |
12 | | cxpcl 24220 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥↑𝑐𝑦) ∈
ℂ) |
13 | 4, 11, 12 | syl2an 493 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ 𝐷) → (𝑥↑𝑐𝑦) ∈ ℂ) |
14 | 13 | rgen2 2958 |
. . 3
⊢
∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ 𝐷 (𝑥↑𝑐𝑦) ∈
ℂ |
15 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) = (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) |
16 | 15 | fmpt2 7126 |
. . 3
⊢
(∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ 𝐷 (𝑥↑𝑐𝑦) ∈ ℂ ↔ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
17 | 14, 16 | mpbi 219 |
. 2
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ |
18 | | cxpcn3.j |
. . . . . . . . . . . . 13
⊢ 𝐽 =
(TopOpen‘ℂfld) |
19 | 18 | cnfldtopon 22396 |
. . . . . . . . . . . 12
⊢ 𝐽 ∈
(TopOn‘ℂ) |
20 | | rpre 11715 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
21 | | rpge0 11721 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 𝑥) |
22 | | elrege0 12149 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
23 | 20, 21, 22 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
(0[,)+∞)) |
24 | 23 | ssriv 3572 |
. . . . . . . . . . . . 13
⊢
ℝ+ ⊆ (0[,)+∞) |
25 | 24, 3 | sstri 3577 |
. . . . . . . . . . . 12
⊢
ℝ+ ⊆ ℂ |
26 | | resttopon 20775 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ℝ+ ⊆ ℂ) → (𝐽 ↾t ℝ+)
∈ (TopOn‘ℝ+)) |
27 | 19, 25, 26 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t
ℝ+) ∈ (TopOn‘ℝ+) |
28 | 27 | toponunii 20547 |
. . . . . . . . . . . 12
⊢
ℝ+ = ∪ (𝐽 ↾t
ℝ+) |
29 | 28 | restid 15917 |
. . . . . . . . . . 11
⊢ ((𝐽 ↾t
ℝ+) ∈ (TopOn‘ℝ+) → ((𝐽 ↾t
ℝ+) ↾t ℝ+) = (𝐽 ↾t
ℝ+)) |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐽 ↾t
ℝ+) ↾t ℝ+) = (𝐽 ↾t
ℝ+) |
31 | 30 | eqcomi 2619 |
. . . . . . . . 9
⊢ (𝐽 ↾t
ℝ+) = ((𝐽
↾t ℝ+) ↾t
ℝ+) |
32 | 27 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝐽 ↾t ℝ+)
∈ (TopOn‘ℝ+)) |
33 | | ssid 3587 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ+ |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ℝ+ ⊆
ℝ+) |
35 | | cxpcn3.l |
. . . . . . . . 9
⊢ 𝐿 = (𝐽 ↾t 𝐷) |
36 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝐽 ∈
(TopOn‘ℂ)) |
37 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝐷 ⊆ ℂ) |
38 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t
ℝ+) = (𝐽
↾t ℝ+) |
39 | 18, 38 | cxpcn2 24287 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+,
𝑦 ∈ ℂ ↦
(𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐽) Cn
𝐽) |
40 | 39 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐽) Cn
𝐽)) |
41 | 31, 32, 34, 35, 36, 37, 40 | cnmpt2res 21290 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐿) Cn
𝐽)) |
42 | | elrege0 12149 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (0[,)+∞) ↔
(𝑢 ∈ ℝ ∧ 0
≤ 𝑢)) |
43 | 42 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (0[,)+∞) →
𝑢 ∈
ℝ) |
44 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → 𝑢 ∈ ℝ) |
45 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑢 ∈ ℝ) |
46 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 0 < 𝑢) |
47 | 45, 46 | elrpd 11745 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑢 ∈ ℝ+) |
48 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑣 ∈ 𝐷) |
49 | | opelxp 5070 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑣〉 ∈
(ℝ+ × 𝐷) ↔ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ 𝐷)) |
50 | 47, 48, 49 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 〈𝑢, 𝑣〉 ∈ (ℝ+ ×
𝐷)) |
51 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ (𝐽
↾t 𝐷)
∈ (TopOn‘𝐷)) |
52 | 19, 10, 51 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t 𝐷) ∈ (TopOn‘𝐷) |
53 | 35, 52 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐿 ∈ (TopOn‘𝐷) |
54 | | txtopon 21204 |
. . . . . . . . . . 11
⊢ (((𝐽 ↾t
ℝ+) ∈ (TopOn‘ℝ+) ∧ 𝐿 ∈ (TopOn‘𝐷)) → ((𝐽 ↾t ℝ+)
×t 𝐿)
∈ (TopOn‘(ℝ+ × 𝐷))) |
55 | 27, 53, 54 | mp2an 704 |
. . . . . . . . . 10
⊢ ((𝐽 ↾t
ℝ+) ×t 𝐿) ∈ (TopOn‘(ℝ+
× 𝐷)) |
56 | 55 | toponunii 20547 |
. . . . . . . . 9
⊢
(ℝ+ × 𝐷) = ∪ ((𝐽 ↾t
ℝ+) ×t 𝐿) |
57 | 56 | cncnpi 20892 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ+,
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐿) Cn
𝐽) ∧ 〈𝑢, 𝑣〉 ∈ (ℝ+ ×
𝐷)) → (𝑥 ∈ ℝ+,
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉)) |
58 | 41, 50, 57 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉)) |
59 | | ssid 3587 |
. . . . . . . 8
⊢ 𝐷 ⊆ 𝐷 |
60 | | resmpt2 6656 |
. . . . . . . 8
⊢
((ℝ+ ⊆ (0[,)+∞) ∧ 𝐷 ⊆ 𝐷) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) = (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))) |
61 | 24, 59, 60 | mp2an 704 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) = (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) |
62 | | cxpcn3.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝐽 ↾t
(0[,)+∞)) |
63 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (0[,)+∞) ⊆ ℂ) → (𝐽 ↾t (0[,)+∞)) ∈
(TopOn‘(0[,)+∞))) |
64 | 19, 3, 63 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t
(0[,)+∞)) ∈ (TopOn‘(0[,)+∞)) |
65 | 62, 64 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐾 ∈
(TopOn‘(0[,)+∞)) |
66 | | ioorp 12122 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) = ℝ+ |
67 | | iooretop 22379 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
68 | 66, 67 | eqeltrri 2685 |
. . . . . . . . . . . . 13
⊢
ℝ+ ∈ (topGen‘ran (,)) |
69 | | retop 22375 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) ∈ Top |
70 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ∈ V |
71 | | restopnb 20789 |
. . . . . . . . . . . . . . 15
⊢
((((topGen‘ran (,)) ∈ Top ∧ (0[,)+∞) ∈ V)
∧ (ℝ+ ∈ (topGen‘ran (,)) ∧
ℝ+ ⊆ (0[,)+∞) ∧ ℝ+ ⊆
ℝ+)) → (ℝ+ ∈ (topGen‘ran (,))
↔ ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)))) |
72 | 69, 70, 71 | mpanl12 714 |
. . . . . . . . . . . . . 14
⊢
((ℝ+ ∈ (topGen‘ran (,)) ∧
ℝ+ ⊆ (0[,)+∞) ∧ ℝ+ ⊆
ℝ+) → (ℝ+ ∈ (topGen‘ran (,))
↔ ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)))) |
73 | 68, 24, 33, 72 | mp3an 1416 |
. . . . . . . . . . . . 13
⊢
(ℝ+ ∈ (topGen‘ran (,)) ↔
ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞))) |
74 | 68, 73 | mpbi 219 |
. . . . . . . . . . . 12
⊢
ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)) |
75 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
76 | 18, 75 | rerest 22415 |
. . . . . . . . . . . . . 14
⊢
((0[,)+∞) ⊆ ℝ → (𝐽 ↾t (0[,)+∞)) =
((topGen‘ran (,)) ↾t (0[,)+∞))) |
77 | 1, 76 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐽 ↾t
(0[,)+∞)) = ((topGen‘ran (,)) ↾t
(0[,)+∞)) |
78 | 62, 77 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐾 = ((topGen‘ran (,))
↾t (0[,)+∞)) |
79 | 74, 78 | eleqtrri 2687 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ 𝐾 |
80 | | toponmax 20543 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (TopOn‘𝐷) → 𝐷 ∈ 𝐿) |
81 | 53, 80 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝐷 ∈ 𝐿 |
82 | | txrest 21244 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) ∧ (ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿)) → ((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) = ((𝐾 ↾t
ℝ+) ×t (𝐿 ↾t 𝐷))) |
83 | 65, 53, 79, 81, 82 | mp4an 705 |
. . . . . . . . . 10
⊢ ((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) = ((𝐾 ↾t ℝ+)
×t (𝐿
↾t 𝐷)) |
84 | 62 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (𝐾 ↾t
ℝ+) = ((𝐽
↾t (0[,)+∞)) ↾t
ℝ+) |
85 | | restabs 20779 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ℝ+ ⊆ (0[,)+∞) ∧ (0[,)+∞) ∈ V)
→ ((𝐽
↾t (0[,)+∞)) ↾t ℝ+) =
(𝐽 ↾t
ℝ+)) |
86 | 19, 24, 70, 85 | mp3an 1416 |
. . . . . . . . . . . 12
⊢ ((𝐽 ↾t
(0[,)+∞)) ↾t ℝ+) = (𝐽 ↾t
ℝ+) |
87 | 84, 86 | eqtri 2632 |
. . . . . . . . . . 11
⊢ (𝐾 ↾t
ℝ+) = (𝐽
↾t ℝ+) |
88 | 53 | toponunii 20547 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ∪
𝐿 |
89 | 88 | restid 15917 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (TopOn‘𝐷) → (𝐿 ↾t 𝐷) = 𝐿) |
90 | 53, 89 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐿 ↾t 𝐷) = 𝐿 |
91 | 87, 90 | oveq12i 6561 |
. . . . . . . . . 10
⊢ ((𝐾 ↾t
ℝ+) ×t (𝐿 ↾t 𝐷)) = ((𝐽 ↾t ℝ+)
×t 𝐿) |
92 | 83, 91 | eqtri 2632 |
. . . . . . . . 9
⊢ ((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) = ((𝐽 ↾t ℝ+)
×t 𝐿) |
93 | 92 | oveq1i 6559 |
. . . . . . . 8
⊢ (((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) CnP 𝐽) = (((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽) |
94 | 93 | fveq1i 6104 |
. . . . . . 7
⊢ ((((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉) = ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉) |
95 | 58, 61, 94 | 3eltr4g 2705 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
96 | | txtopon 21204 |
. . . . . . . . . 10
⊢ ((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) → (𝐾 ×t 𝐿) ∈ (TopOn‘((0[,)+∞)
× 𝐷))) |
97 | 65, 53, 96 | mp2an 704 |
. . . . . . . . 9
⊢ (𝐾 ×t 𝐿) ∈
(TopOn‘((0[,)+∞) × 𝐷)) |
98 | 97 | topontopi 20546 |
. . . . . . . 8
⊢ (𝐾 ×t 𝐿) ∈ Top |
99 | 98 | a1i 11 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝐾 ×t 𝐿) ∈ Top) |
100 | | xpss1 5151 |
. . . . . . . 8
⊢
(ℝ+ ⊆ (0[,)+∞) → (ℝ+
× 𝐷) ⊆
((0[,)+∞) × 𝐷)) |
101 | 24, 100 | mp1i 13 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (ℝ+ × 𝐷) ⊆ ((0[,)+∞)
× 𝐷)) |
102 | | txopn 21215 |
. . . . . . . . . 10
⊢ (((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) ∧ (ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿)) → (ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿)) |
103 | 65, 53, 79, 81, 102 | mp4an 705 |
. . . . . . . . 9
⊢
(ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿) |
104 | | isopn3i 20696 |
. . . . . . . . 9
⊢ (((𝐾 ×t 𝐿) ∈ Top ∧
(ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿)) → ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷)) = (ℝ+
× 𝐷)) |
105 | 98, 103, 104 | mp2an 704 |
. . . . . . . 8
⊢
((int‘(𝐾
×t 𝐿))‘(ℝ+ × 𝐷)) = (ℝ+
× 𝐷) |
106 | 50, 105 | syl6eleqr 2699 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 〈𝑢, 𝑣〉 ∈ ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷))) |
107 | 17 | a1i 11 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
108 | 65 | topontopi 20546 |
. . . . . . . . 9
⊢ 𝐾 ∈ Top |
109 | 53 | topontopi 20546 |
. . . . . . . . 9
⊢ 𝐿 ∈ Top |
110 | 65 | toponunii 20547 |
. . . . . . . . 9
⊢
(0[,)+∞) = ∪ 𝐾 |
111 | 108, 109,
110, 88 | txunii 21206 |
. . . . . . . 8
⊢
((0[,)+∞) × 𝐷) = ∪ (𝐾 ×t 𝐿) |
112 | 19 | toponunii 20547 |
. . . . . . . 8
⊢ ℂ =
∪ 𝐽 |
113 | 111, 112 | cnprest 20903 |
. . . . . . 7
⊢ ((((𝐾 ×t 𝐿) ∈ Top ∧
(ℝ+ × 𝐷) ⊆ ((0[,)+∞) × 𝐷)) ∧ (〈𝑢, 𝑣〉 ∈ ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷)) ∧ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ)) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
114 | 99, 101, 106, 107, 113 | syl22anc 1319 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
115 | 95, 114 | mpbird 246 |
. . . . 5
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
116 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
117 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2) = (if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) |
118 | | eqid 2610 |
. . . . . . . . . . 11
⊢
if((if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) ≤ (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2))), (if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2), (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2)))) = if((if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) ≤ (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2))), (if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2), (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2)))) |
119 | 5, 18, 62, 35, 117, 118 | cxpcn3lem 24288 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ 𝐷 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
120 | 119 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
121 | | 0e0icopnf 12153 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
(0[,)+∞) |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 0 ∈
(0[,)+∞)) |
123 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑎 ∈ (0[,)+∞)) |
124 | 122, 123 | ovresd 6699 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) = (0(abs ∘ − )𝑎)) |
125 | | 0cn 9911 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℂ |
126 | 3, 123 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑎 ∈ ℂ) |
127 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
128 | 127 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
129 | 125, 126,
128 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
130 | | df-neg 10148 |
. . . . . . . . . . . . . . . . . 18
⊢ -𝑎 = (0 − 𝑎) |
131 | 130 | fveq2i 6106 |
. . . . . . . . . . . . . . . . 17
⊢
(abs‘-𝑎) =
(abs‘(0 − 𝑎)) |
132 | 126 | absnegd 14036 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘-𝑎) = (abs‘𝑎)) |
133 | 131, 132 | syl5eqr 2658 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘(0 − 𝑎)) = (abs‘𝑎)) |
134 | 124, 129,
133 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) = (abs‘𝑎)) |
135 | 134 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ↔ (abs‘𝑎) < 𝑑)) |
136 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑣 ∈ 𝐷) |
137 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ 𝐷) |
138 | 136, 137 | ovresd 6699 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) = (𝑣(abs ∘ − )𝑏)) |
139 | 10, 136 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑣 ∈ ℂ) |
140 | 10, 137 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ ℂ) |
141 | 127 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑣(abs ∘ − )𝑏) = (abs‘(𝑣 − 𝑏))) |
142 | 139, 140,
141 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣(abs ∘ − )𝑏) = (abs‘(𝑣 − 𝑏))) |
143 | 138, 142 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) = (abs‘(𝑣 − 𝑏))) |
144 | 143 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑 ↔ (abs‘(𝑣 − 𝑏)) < 𝑑)) |
145 | 135, 144 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (((0((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) ↔ ((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑))) |
146 | | oveq12 6558 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑣) → (𝑥↑𝑐𝑦) = (0↑𝑐𝑣)) |
147 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0↑𝑐𝑣) ∈ V |
148 | 146, 15, 147 | ovmpt2a 6689 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ (0[,)+∞) ∧ 𝑣 ∈ 𝐷) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = (0↑𝑐𝑣)) |
149 | 121, 136,
148 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = (0↑𝑐𝑣)) |
150 | 5 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝐷 ↔ 𝑣 ∈ (◡ℜ “
ℝ+)) |
151 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
152 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℜ
Fn ℂ → (𝑣 ∈
(◡ℜ “ ℝ+)
↔ (𝑣 ∈ ℂ
∧ (ℜ‘𝑣)
∈ ℝ+))) |
153 | 7, 151, 152 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ (◡ℜ “ ℝ+) ↔
(𝑣 ∈ ℂ ∧
(ℜ‘𝑣) ∈
ℝ+)) |
154 | 150, 153 | bitri 263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ 𝐷 ↔ (𝑣 ∈ ℂ ∧ (ℜ‘𝑣) ∈
ℝ+)) |
155 | 154 | simplbi 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ) |
156 | 154 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝐷 → (ℜ‘𝑣) ∈
ℝ+) |
157 | 156 | rpne0d 11753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ 𝐷 → (ℜ‘𝑣) ≠ 0) |
158 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 0 → (ℜ‘𝑣) =
(ℜ‘0)) |
159 | | re0 13740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℜ‘0) = 0 |
160 | 158, 159 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 0 → (ℜ‘𝑣) = 0) |
161 | 160 | necon3i 2814 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℜ‘𝑣)
≠ 0 → 𝑣 ≠
0) |
162 | 157, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ 𝐷 → 𝑣 ≠ 0) |
163 | 155, 162 | 0cxpd 24256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝐷 → (0↑𝑐𝑣) = 0) |
164 | 163 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0↑𝑐𝑣) = 0) |
165 | 149, 164 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = 0) |
166 | | oveq12 6558 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑥↑𝑐𝑦) = (𝑎↑𝑐𝑏)) |
167 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎↑𝑐𝑏) ∈ V |
168 | 166, 15, 167 | ovmpt2a 6689 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ (0[,)+∞) ∧
𝑏 ∈ 𝐷) → (𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏) = (𝑎↑𝑐𝑏)) |
169 | 168 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏) = (𝑎↑𝑐𝑏)) |
170 | 165, 169 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) = (0(abs ∘ − )(𝑎↑𝑐𝑏))) |
171 | 126, 140 | cxpcld 24254 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑎↑𝑐𝑏) ∈ ℂ) |
172 | 127 | cnmetdval 22384 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℂ ∧ (𝑎↑𝑐𝑏) ∈ ℂ) → (0(abs ∘
− )(𝑎↑𝑐𝑏)) = (abs‘(0 − (𝑎↑𝑐𝑏)))) |
173 | 125, 171,
172 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(abs ∘ − )(𝑎↑𝑐𝑏)) = (abs‘(0 −
(𝑎↑𝑐𝑏)))) |
174 | | df-neg 10148 |
. . . . . . . . . . . . . . . . 17
⊢ -(𝑎↑𝑐𝑏) = (0 − (𝑎↑𝑐𝑏)) |
175 | 174 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘-(𝑎↑𝑐𝑏)) = (abs‘(0 − (𝑎↑𝑐𝑏))) |
176 | 171 | absnegd 14036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘-(𝑎↑𝑐𝑏)) = (abs‘(𝑎↑𝑐𝑏))) |
177 | 175, 176 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘(0 − (𝑎↑𝑐𝑏))) = (abs‘(𝑎↑𝑐𝑏))) |
178 | 170, 173,
177 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) = (abs‘(𝑎↑𝑐𝑏))) |
179 | 178 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒 ↔ (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
180 | 145, 179 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((((0((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
181 | 180 | 2ralbidva 2971 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝐷 → (∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
182 | 181 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝐷 → (∃𝑑 ∈ ℝ+ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
183 | 182 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → (∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
184 | 120, 183 | mpbird 246 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)) |
185 | | cnxmet 22386 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
186 | 185 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝐷 → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
187 | | xmetres2 21976 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (0[,)+∞)
⊆ ℂ) → ((abs ∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞))) ∈ (∞Met‘(0[,)+∞))) |
188 | 186, 3, 187 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞))) ∈
(∞Met‘(0[,)+∞))) |
189 | | xmetres2 21976 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐷
× 𝐷)) ∈
(∞Met‘𝐷)) |
190 | 186, 10, 189 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ((abs ∘ − ) ↾
(𝐷 × 𝐷)) ∈
(∞Met‘𝐷)) |
191 | 121 | a1i 11 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → 0 ∈
(0[,)+∞)) |
192 | | id 22 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → 𝑣 ∈ 𝐷) |
193 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ ((0[,)+∞) × (0[,)+∞))) = ((abs
∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞))) |
194 | 18 | cnfldtopn 22395 |
. . . . . . . . . . . . 13
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
195 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘((abs ∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞)))) = (MetOpen‘((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))) |
196 | 193, 194,
195 | metrest 22139 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (0[,)+∞)
⊆ ℂ) → (𝐽
↾t (0[,)+∞)) = (MetOpen‘((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞))))) |
197 | 185, 3, 196 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t
(0[,)+∞)) = (MetOpen‘((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))) |
198 | 62, 197 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))) |
199 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (𝐷 × 𝐷)) = ((abs ∘ − ) ↾ (𝐷 × 𝐷)) |
200 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐷 × 𝐷))) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) |
201 | 199, 194,
200 | metrest 22139 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → (𝐽 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) |
202 | 185, 10, 201 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t 𝐷) = (MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) |
203 | 35, 202 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐿 = (MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) |
204 | 198, 203,
194 | txmetcnp 22162 |
. . . . . . . . 9
⊢ (((((abs
∘ − ) ↾ ((0[,)+∞) × (0[,)+∞))) ∈
(∞Met‘(0[,)+∞)) ∧ ((abs ∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷) ∧ (abs ∘ − )
∈ (∞Met‘ℂ)) ∧ (0 ∈ (0[,)+∞) ∧ 𝑣 ∈ 𝐷)) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)))) |
205 | 188, 190,
186, 191, 192, 204 | syl32anc 1326 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)))) |
206 | 116, 184,
205 | mpbir2and 959 |
. . . . . . 7
⊢ (𝑣 ∈ 𝐷 → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉)) |
207 | 206 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉)) |
208 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → 0 = 𝑢) |
209 | 208 | opeq1d 4346 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → 〈0, 𝑣〉 = 〈𝑢, 𝑣〉) |
210 | 209 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) = (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
211 | 207, 210 | eleqtrd 2690 |
. . . . 5
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
212 | 42 | simprbi 479 |
. . . . . . 7
⊢ (𝑢 ∈ (0[,)+∞) → 0
≤ 𝑢) |
213 | 212 | adantr 480 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → 0 ≤ 𝑢) |
214 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
215 | | leloe 10003 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ) → (0 ≤ 𝑢 ↔ (0 < 𝑢 ∨ 0 = 𝑢))) |
216 | 214, 44, 215 | sylancr 694 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (0 ≤ 𝑢 ↔ (0 < 𝑢 ∨ 0 = 𝑢))) |
217 | 213, 216 | mpbid 221 |
. . . . 5
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (0 < 𝑢 ∨ 0 = 𝑢)) |
218 | 115, 211,
217 | mpjaodan 823 |
. . . 4
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
219 | 218 | rgen2 2958 |
. . 3
⊢
∀𝑢 ∈
(0[,)+∞)∀𝑣
∈ 𝐷 (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) |
220 | | fveq2 6103 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) = (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
221 | 220 | eleq2d 2673 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) ↔ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
222 | 221 | ralxp 5185 |
. . 3
⊢
(∀𝑧 ∈
((0[,)+∞) × 𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) ↔ ∀𝑢 ∈ (0[,)+∞)∀𝑣 ∈ 𝐷 (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
223 | 219, 222 | mpbir 220 |
. 2
⊢
∀𝑧 ∈
((0[,)+∞) × 𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) |
224 | | cncnp 20894 |
. . 3
⊢ (((𝐾 ×t 𝐿) ∈
(TopOn‘((0[,)+∞) × 𝐷)) ∧ 𝐽 ∈ (TopOn‘ℂ)) →
((𝑥 ∈ (0[,)+∞),
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑧 ∈ ((0[,)+∞) ×
𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧)))) |
225 | 97, 19, 224 | mp2an 704 |
. 2
⊢ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑧 ∈ ((0[,)+∞) ×
𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧))) |
226 | 17, 223, 225 | mpbir2an 957 |
1
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) |