Metamath Proof Explorer

Theorem bnnlm

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

Ref Expression
Assertion bnnlm ⊢ W ∈ Ban → W ∈ NrmMod

Proof

Step Hyp Ref Expression
1 bnnvc ⊢ W ∈ Ban → W ∈ NrmVec
2 nvcnlm ⊢ W ∈ NrmVec → W ∈ NrmMod
3 1 2 syl ⊢ W ∈ Ban → W ∈ NrmMod