This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The set of scalars of a left vector space is a division ring.
(Contributed by NM, 17-Apr-2014)
|
|
Ref |
Expression |
|
Hypothesis |
islvec.1 |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
|
Assertion |
lvecdrng |
⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
islvec.1 |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
| 2 |
1
|
islvec |
⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing ) ) |
| 3 |
2
|
simprbi |
⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing ) |