Metamath Proof Explorer


Theorem nvclvec

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

Ref Expression
Assertion nvclvec W NrmVec W LVec

Proof

Step Hyp Ref Expression
1 isnvc W NrmVec W NrmMod W LVec
2 1 simprbi W NrmVec W LVec