This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \cap LVec$

Step	Hyp	Ref	Expression
0		cnvc	$class NrmVec$
1		cnlm	$class NrmMod$
2		clvec	$class LVec$
3	1 2	cin	$class (NrmMod \cap LVec)$
4	0 3	wceq	$wff NrmVec = NrmMod \cap LVec$