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 ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )

Proof

Step Hyp Ref Expression
1 eqid ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
2 eqid ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 )
3 1 2 iscbn ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ ( IndMet ‘ 𝑈 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑈 ) ) ) )
4 3 simplbi ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )