Metamath Proof Explorer


Theorem nmcvcn

Description: The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007) (Proof shortened by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses nmcvcn.1 𝑁 = ( normCV𝑈 )
nmcvcn.2 𝐶 = ( IndMet ‘ 𝑈 )
nmcvcn.j 𝐽 = ( MetOpen ‘ 𝐶 )
nmcvcn.k 𝐾 = ( topGen ‘ ran (,) )
Assertion nmcvcn ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

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 𝐾 ) )