Metamath Proof Explorer


Theorem bnnlm

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

Ref Expression
Assertion bnnlm WBanWNrmMod

Proof

Step Hyp Ref Expression
1 bnnvc WBanWNrmVec
2 nvcnlm WNrmVecWNrmMod
3 1 2 syl WBanWNrmMod