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