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\in \mathrm{CBan}\to U\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
2		eqid	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{IndMet}\left(U\right)$$
3	1 2	iscbn	$$⊢U\in \mathrm{CBan}\leftrightarrow \left(U\in \mathrm{NrmCVec}\wedge \mathrm{IndMet}\left(U\right)\in \mathrm{CMet}\left(\mathrm{BaseSet}\left(U\right)\right)\right)$$
4	3	simplbi	$$⊢U\in \mathrm{CBan}\to U\in \mathrm{NrmCVec}$$