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	⊢ NrmVec = ( NrmMod ∩ LVec )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnvc	⊢ NrmVec
1		cnlm	⊢ NrmMod
2		clvec	⊢ LVec
3	1 2	cin	⊢ ( NrmMod ∩ LVec )
4	0 3	wceq	⊢ NrmVec = ( NrmMod ∩ LVec )