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 UCBanUNrmCVec

Proof

Step Hyp Ref Expression
1 eqid BaseSetU=BaseSetU
2 eqid IndMetU=IndMetU
3 1 2 iscbn UCBanUNrmCVecIndMetUCMetBaseSetU
4 3 simplbi UCBanUNrmCVec