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

Metamath Proof Explorer

Theorem bnnvc

Description: A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion bnnvc ⊢ W ∈ Ban → W ∈ NrmVec

Proof

Step Hyp Ref Expression
1 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
2 1 isbn ⊢ W ∈ Ban ↔ W ∈ NrmVec ∧ W ∈ CMetSp ∧ Scalar ⁡ W ∈ CMetSp
3 2 simp1bi ⊢ W ∈ Ban → W ∈ NrmVec