Definition df-nvc 24912

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 24906	. 2 class NrmVec
2		cnlm 24905	. . 3 class NrmMod
3		clvec 21383	. . 3 class LVec
4	2, 3	cin 4089	. 2 class (NrmMod ∩ LVec)
5	1, 4	wceq 1569	1 wff NrmVec = (NrmMod ∩ LVec)

This definition is used by:  isnvc  25020