Definition df-nvc 24781

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

Assertion

Ref	Expression
df-nvc	⊢ NrmVec = (NrmMod ∩ LVec)

Detailed syntax breakdown of Definition df-nvc

Step	Hyp	Ref	Expression
1		cnvc 24775	. 2 class NrmVec
2		cnlm 24774	. . 3 class NrmMod
3		clvec 21260	. . 3 class LVec
4	2, 3	cin 3907	. 2 class (NrmMod ∩ LVec)
5	1, 4	wceq 1570	1 wff NrmVec = (NrmMod ∩ LVec)

This definition is used by:  isnvc  24889