Step |
Hyp |
Ref |
Expression |
1 |
|
nmcvcn.1 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
2 |
|
nmcvcn.2 |
⊢ 𝐶 = ( IndMet ‘ 𝑈 ) |
3 |
|
nmcvcn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) |
4 |
|
nmcvcn.k |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
5 |
|
eqid |
⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 ) |
6 |
5 1
|
nvf |
⊢ ( 𝑈 ∈ NrmCVec → 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ℝ ) |
7 |
|
simprr |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑒 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ+ ) |
8 |
5 1
|
nvcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑥 ) ∈ ℝ ) |
9 |
8
|
ex |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑁 ‘ 𝑥 ) ∈ ℝ ) ) |
10 |
5 1
|
nvcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) |
11 |
10
|
ex |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) ) |
12 |
9 11
|
anim12d |
⊢ ( 𝑈 ∈ NrmCVec → ( ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) ) ) |
13 |
|
eqid |
⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) |
14 |
13
|
remet |
⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) |
15 |
|
metcl |
⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) ∧ ( 𝑁 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ) |
16 |
14 15
|
mp3an1 |
⊢ ( ( ( 𝑁 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ) |
17 |
12 16
|
syl6 |
⊢ ( 𝑈 ∈ NrmCVec → ( ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ) ) |
18 |
17
|
3impib |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ) |
19 |
5 2
|
imsmet |
⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ) |
20 |
|
metcl |
⊢ ( ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) |
21 |
19 20
|
syl3an1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) |
22 |
|
eqid |
⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 ) |
23 |
|
eqid |
⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 ) |
24 |
5 22 23 1
|
nvabs |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( abs ‘ ( ( 𝑁 ‘ 𝑥 ) − ( 𝑁 ‘ 𝑦 ) ) ) ≤ ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ) |
25 |
12
|
3impib |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) ) |
26 |
13
|
remetdval |
⊢ ( ( ( 𝑁 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑁 ‘ 𝑥 ) − ( 𝑁 ‘ 𝑦 ) ) ) ) |
27 |
25 26
|
syl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑁 ‘ 𝑥 ) − ( 𝑁 ‘ 𝑦 ) ) ) ) |
28 |
5 22 23 1 2
|
imsdval2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑦 ) = ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ) |
29 |
24 27 28
|
3brtr4d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ) |
30 |
18 21 29
|
jca31 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ) ) |
31 |
30
|
3expa |
⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ) ) |
32 |
|
rpre |
⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ ) |
33 |
|
lelttr |
⊢ ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ∧ ( 𝑥 𝐶 𝑦 ) < 𝑒 ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
34 |
33
|
3expa |
⊢ ( ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) ∧ 𝑒 ∈ ℝ ) → ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ∧ ( 𝑥 𝐶 𝑦 ) < 𝑒 ) → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
35 |
34
|
expdimp |
⊢ ( ( ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) ∧ 𝑒 ∈ ℝ ) ∧ ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ) → ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
36 |
35
|
an32s |
⊢ ( ( ( ( ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑥 𝐶 𝑦 ) ) ∧ 𝑒 ∈ ℝ ) → ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
37 |
31 32 36
|
syl2an |
⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑒 ∈ ℝ+ ) → ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
38 |
37
|
ex |
⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑒 ∈ ℝ+ → ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) ) |
39 |
38
|
ralrimdva |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑒 ∈ ℝ+ → ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) ) |
40 |
39
|
impr |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑒 ∈ ℝ+ ) ) → ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
41 |
|
breq2 |
⊢ ( 𝑑 = 𝑒 → ( ( 𝑥 𝐶 𝑦 ) < 𝑑 ↔ ( 𝑥 𝐶 𝑦 ) < 𝑒 ) ) |
42 |
41
|
rspceaimv |
⊢ ( ( 𝑒 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑒 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑑 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
43 |
7 40 42
|
syl2anc |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑒 ∈ ℝ+ ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑑 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
44 |
43
|
ralrimivva |
⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑑 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) |
45 |
5 2
|
imsxmet |
⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ) |
46 |
13
|
rexmet |
⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) |
47 |
|
eqid |
⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) |
48 |
13 47
|
tgioo |
⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) |
49 |
4 48
|
eqtri |
⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) |
50 |
3 49
|
metcn |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ) → ( 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑑 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) ) ) |
51 |
45 46 50
|
sylancl |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑦 ) < 𝑑 → ( ( 𝑁 ‘ 𝑥 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝑁 ‘ 𝑦 ) ) < 𝑒 ) ) ) ) |
52 |
6 44 51
|
mpbir2and |
⊢ ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ) |