Theorem lvecdrng 19870

Description: The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.)

Hypothesis

Ref	Expression
islvec.1	⊢ 𝐹 = (Scalar‘𝑊)

Assertion

Ref	Expression
lvecdrng	⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Proof of Theorem lvecdrng

Step	Hyp	Ref	Expression
1		islvec.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	islvec 19869	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
3	2	simprbi 500	1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  Scalarcsca 16560  DivRingcdr 19495  LModclmod 19627  LVecclvec 19867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-lvec 19868

This theorem is referenced by:  lsslvec  19872  lvecvs0or  19873  lssvs0or  19875  lvecinv  19878  lspsnvs  19879  lspsneq  19887  lspfixed  19893  lspexch  19894  lspsolv  19908  islbs2  19919  islbs3  19920  obsne0  20414  islinds4  20524  nvctvc  23306  lssnvc  23308  cvsunit  23736  cvsdivcl  23738  cphsubrg  23785  cphreccl  23786  cphqss  23793  phclm  23836  ipcau2  23838  tcphcph  23841  hlprlem  23971  ishl2  23974  0nellinds  30986  lmhmlvec2  31105  lfl1  36366  lkrsc  36393  eqlkr3  36397  lkrlsp  36398  lkrshp  36401  lduallvec  36450  dochkr1  38774  dochkr1OLDN  38775  lcfl7lem  38795  lclkrlem2m  38815  lclkrlem2o  38817  lclkrlem2p  38818  lcfrlem1  38838  lcfrlem2  38839  lcfrlem3  38840  lcfrlem29  38867  lcfrlem31  38869  lcfrlem33  38871  mapdpglem17N  38984  mapdpglem18  38985  mapdpglem19  38986  mapdpglem21  38988  mapdpglem22  38989  hdmapip1  39212  hgmapvvlem1  39219  hgmapvvlem2  39220  hgmapvvlem3  39221  prjspersym  39601  lincreslvec3  44891  isldepslvec2  44894