Theorem rlmlvec

Description: The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	rlmlvec	⊢ ( 𝑅 ∈ DivRing → ( ringLMod ‘ 𝑅 ) ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
2		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
3	1 2	syl	⊢ ( 𝑅 ∈ DivRing → ( ringLMod ‘ 𝑅 ) ∈ LMod )
4		rlmsca	⊢ ( 𝑅 ∈ DivRing → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
5		id	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ DivRing )
6	4 5	eqeltrrd	⊢ ( 𝑅 ∈ DivRing → ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ∈ DivRing )
7		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
8	7	islvec	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LVec ↔ ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ∈ DivRing ) )
9	3 6 8	sylanbrc	⊢ ( 𝑅 ∈ DivRing → ( ringLMod ‘ 𝑅 ) ∈ LVec )