This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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