df-nvc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-nvc		Structured version Visualization version GIF version

Definition df-nvc 23724

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 23718	. 2 class NrmVec
2		cnlm 23717	. . 3 class NrmMod
3		clvec 20345	. . 3 class LVec
4	2, 3	cin 3890	. 2 class (NrmMod ∩ LVec)
5	1, 4	wceq 1541	1 wff NrmVec = (NrmMod ∩ LVec)

Colors of variables: wff setvar class

This definition is referenced by: isnvc 23840