Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
2 | | nmcvcn.1 |
. . 3
⊢ 𝑁 =
(normCV‘𝑈) |
3 | 1, 2 | nvf 27515 |
. 2
⊢ (𝑈 ∈ NrmCVec → 𝑁:(BaseSet‘𝑈)⟶ℝ) |
4 | | simprr 796 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑒 ∈ ℝ+)) → 𝑒 ∈
ℝ+) |
5 | 1, 2 | nvcl 27516 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈)) → (𝑁‘𝑥) ∈ ℝ) |
6 | 5 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (𝑥 ∈ (BaseSet‘𝑈) → (𝑁‘𝑥) ∈ ℝ)) |
7 | 1, 2 | nvcl 27516 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑁‘𝑦) ∈ ℝ) |
8 | 7 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ NrmCVec → (𝑦 ∈ (BaseSet‘𝑈) → (𝑁‘𝑦) ∈ ℝ)) |
9 | 6, 8 | anim12d 586 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmCVec → ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥) ∈ ℝ ∧ (𝑁‘𝑦) ∈ ℝ))) |
10 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
11 | 10 | remet 22593 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(Met‘ℝ) |
12 | | metcl 22137 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
∧ (𝑁‘𝑥) ∈ ℝ ∧ (𝑁‘𝑦) ∈ ℝ) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ) |
13 | 11, 12 | mp3an1 1411 |
. . . . . . . . . . . 12
⊢ (((𝑁‘𝑥) ∈ ℝ ∧ (𝑁‘𝑦) ∈ ℝ) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ) |
14 | 9, 13 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec → ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ)) |
15 | 14 | 3impib 1262 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ) |
16 | | nmcvcn.2 |
. . . . . . . . . . . 12
⊢ 𝐶 = (IndMet‘𝑈) |
17 | 1, 16 | imsmet 27546 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈
(Met‘(BaseSet‘𝑈))) |
18 | | metcl 22137 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈
(Met‘(BaseSet‘𝑈)) ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑦) ∈ ℝ) |
19 | 17, 18 | syl3an1 1359 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑦) ∈ ℝ) |
20 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
21 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
22 | 1, 20, 21, 2 | nvabs 27527 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (abs‘((𝑁‘𝑥) − (𝑁‘𝑦))) ≤ (𝑁‘(𝑥( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑦)))) |
23 | 9 | 3impib 1262 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥) ∈ ℝ ∧ (𝑁‘𝑦) ∈ ℝ)) |
24 | 10 | remetdval 22592 |
. . . . . . . . . . . 12
⊢ (((𝑁‘𝑥) ∈ ℝ ∧ (𝑁‘𝑦) ∈ ℝ) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) = (abs‘((𝑁‘𝑥) − (𝑁‘𝑦)))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) = (abs‘((𝑁‘𝑥) − (𝑁‘𝑦)))) |
26 | 1, 20, 21, 2, 16 | imsdval2 27542 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑦) = (𝑁‘(𝑥( +𝑣 ‘𝑈)(-1(
·𝑠OLD ‘𝑈)𝑦)))) |
27 | 22, 25, 26 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦)) |
28 | 15, 19, 27 | jca31 557 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ) ∧ ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦))) |
29 | 28 | 3expa 1265 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → ((((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ) ∧ ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦))) |
30 | | rpre 11839 |
. . . . . . . 8
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ) |
31 | | lelttr 10128 |
. . . . . . . . . . 11
⊢ ((((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦) ∧ (𝑥𝐶𝑦) < 𝑒) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
32 | 31 | 3expa 1265 |
. . . . . . . . . 10
⊢
(((((𝑁‘𝑥)((abs ∘ − ) ↾
(ℝ × ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ) ∧ 𝑒 ∈ ℝ) → ((((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦) ∧ (𝑥𝐶𝑦) < 𝑒) → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
33 | 32 | expdimp 453 |
. . . . . . . . 9
⊢
((((((𝑁‘𝑥)((abs ∘ − ) ↾
(ℝ × ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ) ∧ 𝑒 ∈ ℝ) ∧ ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦)) → ((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
34 | 33 | an32s 846 |
. . . . . . . 8
⊢
((((((𝑁‘𝑥)((abs ∘ − ) ↾
(ℝ × ℝ))(𝑁‘𝑦)) ∈ ℝ ∧ (𝑥𝐶𝑦) ∈ ℝ) ∧ ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) ≤ (𝑥𝐶𝑦)) ∧ 𝑒 ∈ ℝ) → ((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
35 | 29, 30, 34 | syl2an 494 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑦 ∈ (BaseSet‘𝑈)) ∧ 𝑒 ∈ ℝ+) → ((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
36 | 35 | ex 450 |
. . . . . 6
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑒 ∈ ℝ+ → ((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒))) |
37 | 36 | ralrimdva 2969 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ (BaseSet‘𝑈)) → (𝑒 ∈ ℝ+ →
∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒))) |
38 | 37 | impr 649 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑒 ∈ ℝ+)) →
∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
39 | | breq2 4657 |
. . . . . . 7
⊢ (𝑑 = 𝑒 → ((𝑥𝐶𝑦) < 𝑑 ↔ (𝑥𝐶𝑦) < 𝑒)) |
40 | 39 | imbi1d 331 |
. . . . . 6
⊢ (𝑑 = 𝑒 → (((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒) ↔ ((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒))) |
41 | 40 | ralbidv 2986 |
. . . . 5
⊢ (𝑑 = 𝑒 → (∀𝑦 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒) ↔ ∀𝑦 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒))) |
42 | 41 | rspcev 3309 |
. . . 4
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑒 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
43 | 4, 38, 42 | syl2anc 693 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑒 ∈ ℝ+)) →
∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
44 | 43 | ralrimivva 2971 |
. 2
⊢ (𝑈 ∈ NrmCVec →
∀𝑥 ∈
(BaseSet‘𝑈)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)) |
45 | 1, 16 | imsxmet 27547 |
. . 3
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈
(∞Met‘(BaseSet‘𝑈))) |
46 | 10 | rexmet 22594 |
. . 3
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
47 | | nmcvcn.j |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐶) |
48 | | nmcvcn.k |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
49 | | eqid 2622 |
. . . . . 6
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
50 | 10, 49 | tgioo 22599 |
. . . . 5
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
51 | 48, 50 | eqtri 2644 |
. . . 4
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
52 | 47, 51 | metcn 22348 |
. . 3
⊢ ((𝐶 ∈
(∞Met‘(BaseSet‘𝑈)) ∧ ((abs ∘ − ) ↾
(ℝ × ℝ)) ∈ (∞Met‘ℝ)) → (𝑁 ∈ (𝐽 Cn 𝐾) ↔ (𝑁:(BaseSet‘𝑈)⟶ℝ ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)))) |
53 | 45, 46, 52 | sylancl 694 |
. 2
⊢ (𝑈 ∈ NrmCVec → (𝑁 ∈ (𝐽 Cn 𝐾) ↔ (𝑁:(BaseSet‘𝑈)⟶ℝ ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑦) < 𝑑 → ((𝑁‘𝑥)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝑁‘𝑦)) < 𝑒)))) |
54 | 3, 44, 53 | mpbir2and 957 |
1
⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾)) |