Definition df-nvc

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

	Ref	Expression
Assertion	df-nvc	$$⊢\mathrm{NrmVec}=\mathrm{NrmMod}\cap \mathrm{LVec}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnvc	$$class\mathrm{NrmVec}$$
1		cnlm	$$class\mathrm{NrmMod}$$
2		clvec	$$class\mathrm{LVec}$$
3	1 2	cin	$$class\left(\mathrm{NrmMod}\cap \mathrm{LVec}\right)$$
4	0 3	wceq	$$wff\mathrm{NrmVec}=\mathrm{NrmMod}\cap \mathrm{LVec}$$