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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	isnvc2	⊢ ( 𝑊 ∈ NrmVec ↔ ( 𝑊 ∈ NrmMod ∧ 𝐹 ∈ DivRing ) )

Proof

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