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

Metamath Proof Explorer

Theorem bncms

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

Ref Expression
Assertion bncms ⊢ W ∈ Ban → W ∈ CMetSp

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 simp2bi ⊢ W ∈ Ban → W ∈ CMetSp