This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ CBan → U ∈ NrmCVec

Proof

Step Hyp Ref Expression
1 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
2 eqid ⊢ IndMet ⁡ U = IndMet ⁡ U
3 1 2 iscbn ⊢ U ∈ CBan ↔ U ∈ NrmCVec ∧ IndMet ⁡ U ∈ CMet ⁡ BaseSet ⁡ U
4 3 simplbi ⊢ U ∈ CBan → U ∈ NrmCVec