Metamath Proof Explorer


Theorem isnvc2

Description: A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypothesis isnvc2.1
|- F = ( Scalar ` W )
Assertion isnvc2
|- ( W e. NrmVec <-> ( W e. NrmMod /\ F e. DivRing ) )

Proof

Step Hyp Ref Expression
1 isnvc2.1
 |-  F = ( Scalar ` W )
2 isnvc
 |-  ( W e. NrmVec <-> ( W e. NrmMod /\ W e. LVec ) )
3 nlmlmod
 |-  ( W e. NrmMod -> W e. LMod )
4 1 islvec
 |-  ( W e. LVec <-> ( W e. LMod /\ F e. DivRing ) )
5 4 baib
 |-  ( W e. LMod -> ( W e. LVec <-> F e. DivRing ) )
6 3 5 syl
 |-  ( W e. NrmMod -> ( W e. LVec <-> F e. DivRing ) )
7 6 pm5.32i
 |-  ( ( W e. NrmMod /\ W e. LVec ) <-> ( W e. NrmMod /\ F e. DivRing ) )
8 2 7 bitri
 |-  ( W e. NrmVec <-> ( W e. NrmMod /\ F e. DivRing ) )