This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmlvec

Description: The free module over a division ring is a left vector space. (Contributed by Steven Nguyen, 29-Apr-2023)

Ref Expression
Hypothesis frlmlvec.1 ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion frlmlvec ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LVec )

Proof

Step Hyp Ref Expression
1 frlmlvec.1 ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
4 2 3 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
5 1 frlmsca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
6 simpl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ DivRing )
7 5 6 eqeltrrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝐹 ) ∈ DivRing )
8 eqid ⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
9 8 islvec ⊢ ( 𝐹 ∈ LVec ↔ ( 𝐹 ∈ LMod ∧ ( Scalar ‘ 𝐹 ) ∈ DivRing ) )
10 4 7 9 sylanbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LVec )