Definition df-nvc 22392

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 i^i LVec )

Detailed syntax breakdown of Definition df-nvc

Step	Hyp	Ref	Expression
1		cnvc 22386	. 2 class NrmVec
2		cnlm 22385	. . 3 class NrmMod
3		clvec 19102	. . 3 class LVec
4	2, 3	cin 3573	. 2 class (NrmMod i^i LVec )
5	1, 4	wceq 1483	1 wff NrmVec = (NrmMod i^i LVec )

This definition is referenced by:  isnvc  22499