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 = ( 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 ) )