Theorem bnnv

Description: Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007) Use bnnvc instead. (New usage is discouraged.)

	Ref	Expression
Assertion	bnnv	|- ( U e. CBan -> U e. NrmCVec )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
2		eqid	|- ( IndMet ` U ) = ( IndMet ` U )
3	1 2	iscbn	|- ( U e. CBan <-> ( U e. NrmCVec /\ ( IndMet ` U ) e. ( CMet ` ( BaseSet ` U ) ) ) )
4	3	simplbi	|- ( U e. CBan -> U e. NrmCVec )