Theorem nvcnlm

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

	Ref	Expression
Assertion	nvcnlm	$$⊢W\in \mathrm{NrmVec}\to W\in \mathrm{NrmMod}$$

Proof

Step	Hyp	Ref	Expression
1		isnvc	$$⊢W\in \mathrm{NrmVec}\leftrightarrow \left(W\in \mathrm{NrmMod}\wedge W\in \mathrm{LVec}\right)$$
2	1	simplbi	$$⊢W\in \mathrm{NrmVec}\to W\in \mathrm{NrmMod}$$