Description: The norm of a normed complex vector space is a continuous function to CC . (For RR , see nmcvcn .) (Contributed by NM, 12-Aug-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nmcnc.1 | ⊢ 𝑁 = ( normCV ‘ 𝑈 ) | |
nmcnc.2 | ⊢ 𝐶 = ( IndMet ‘ 𝑈 ) | ||
nmcnc.j | ⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) | ||
nmcnc.k | ⊢ 𝐾 = ( TopOpen ‘ ℂfld ) | ||
Assertion | nmcnc | ⊢ ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmcnc.1 | ⊢ 𝑁 = ( normCV ‘ 𝑈 ) | |
2 | nmcnc.2 | ⊢ 𝐶 = ( IndMet ‘ 𝑈 ) | |
3 | nmcnc.j | ⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) | |
4 | nmcnc.k | ⊢ 𝐾 = ( TopOpen ‘ ℂfld ) | |
5 | 4 | cnfldtop | ⊢ 𝐾 ∈ Top |
6 | cnrest2r | ⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 ) ) | |
7 | 5 6 | ax-mp | ⊢ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 ) |
8 | 4 | tgioo2 | ⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ ) |
9 | 8 | eqcomi | ⊢ ( 𝐾 ↾t ℝ ) = ( topGen ‘ ran (,) ) |
10 | 1 2 3 9 | nmcvcn | ⊢ ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ) |
11 | 7 10 | sselid | ⊢ ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) ) |