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∈NrmVec↔W∈NrmMod∧F∈DivRing

Proof

Step Hyp Ref Expression
1 isnvc2.1 ⊢F=Scalar⁡W
2 isnvc ⊢W∈NrmVec↔W∈NrmMod∧W∈LVec
3 nlmlmod ⊢W∈NrmMod→W∈LMod
4 1 islvec ⊢W∈LVec↔W∈LMod∧F∈DivRing
5 4 baib ⊢W∈LMod→W∈LVec↔F∈DivRing
6 3 5 syl ⊢W∈NrmMod→W∈LVec↔F∈DivRing
7 6 pm5.32i ⊢W∈NrmMod∧W∈LVec↔W∈NrmMod∧F∈DivRing
8 2 7 bitri ⊢W∈NrmVec↔W∈NrmMod∧F∈DivRing