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 = ( normCV ` U )
	nmcnc.2	|- C = ( IndMet ` U )
	nmcnc.j	|- J = ( MetOpen ` C )
	nmcnc.k	|- K = ( TopOpen ` CCfld )
Assertion	nmcnc	|- ( U e. NrmCVec -> N e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		nmcnc.1	|- N = ( normCV ` U )
2		nmcnc.2	|- C = ( IndMet ` U )
3		nmcnc.j	|- J = ( MetOpen ` C )
4		nmcnc.k	|- K = ( TopOpen ` CCfld )
5	4	cnfldtop	|- K e. Top
6		cnrest2r	|- ( K e. Top -> ( J Cn ( K |`t RR ) ) C_ ( J Cn K ) )
7	5 6	ax-mp	|- ( J Cn ( K |`t RR ) ) C_ ( J Cn K )
8	4	tgioo2	|- ( topGen ` ran (,) ) = ( K |`t RR )
9	8	eqcomi	|- ( K |`t RR ) = ( topGen ` ran (,) )
10	1 2 3 9	nmcvcn	|- ( U e. NrmCVec -> N e. ( J Cn ( K |`t RR ) ) )
11	7 10	sselid	|- ( U e. NrmCVec -> N e. ( J Cn K ) )