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 𝑁 = ( normCV𝑈 )
nmcnc.2 𝐶 = ( IndMet ‘ 𝑈 )
nmcnc.j 𝐽 = ( MetOpen ‘ 𝐶 )
nmcnc.k 𝐾 = ( TopOpen ‘ ℂfld )
Assertion nmcnc ( 𝑈 ∈ NrmCVec → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

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