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 LVec

Detailed syntax breakdown

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