Metamath Proof Explorer


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 )