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

Metamath Proof Explorer

Theorem nmcnc

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 ⊢ N = norm CV ⁡ U
nmcnc.2 ⊢ C = IndMet ⁡ U
nmcnc.j ⊢ J = MetOpen ⁡ C
nmcnc.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion nmcnc ⊢ U ∈ NrmCVec → N ∈ J Cn K

Proof

Step Hyp Ref Expression
1 nmcnc.1 ⊢ N = norm CV ⁡ U
2 nmcnc.2 ⊢ C = IndMet ⁡ U
3 nmcnc.j ⊢ J = MetOpen ⁡ C
4 nmcnc.k ⊢ K = TopOpen ⁡ ℂ fld
5 4 cnfldtop ⊢ K ∈ Top
6 cnrest2r ⊢ K ∈ Top → J Cn K ↾ 𝑡 ℝ ⊆ J Cn K
7 5 6 ax-mp ⊢ J Cn K ↾ 𝑡 ℝ ⊆ J Cn K
8 4 tgioo2 ⊢ topGen ⁡ ran ⁡ . = K ↾ 𝑡 ℝ
9 8 eqcomi ⊢ K ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
10 1 2 3 9 nmcvcn ⊢ U ∈ NrmCVec → N ∈ J Cn K ↾ 𝑡 ℝ
11 7 10 sselid ⊢ U ∈ NrmCVec → N ∈ J Cn K