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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnvc 
 |-  NrmVec
1 cnlm 
 |-  NrmMod
2 clvec 
 |-  LVec
3 1 2 cin 
 |-  ( NrmMod i^i LVec )
4 0 3 wceq 
 |-  NrmVec = ( NrmMod i^i LVec )