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