Theorem lvecdrng 21145

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 21144	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
3	2	simprbi 500	1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  Scalarcsca 17265  DivRingcdr 20751  LModclmod 20900  LVecclvec 21142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-lvec 21143

This theorem is referenced by:  lsslvec  21149  lvecvs0or  21151  lssvs0or  21153  lvecinv  21156  lspsnvs  21157  lspsneq  21165  lspfixed  21171  lspexch  21172  lspsolv  21186  islbs2  21197  islbs3  21198  obsne0  21750  islinds4  21860  nvctvc  24733  lssnvc  24735  cvsunit  25166  cvsdivcl  25168  cphsubrg  25215  cphreccl  25216  cphqss  25223  phclm  25267  ipcau2  25269  tcphcph  25272  hlprlem  25402  ishl2  25405  quslvec  33500  0nellinds  33510  lmhmlvec2  33870  dimlssid  33883  lfl1  39642  lkrsc  39669  eqlkr3  39673  lkrlsp  39674  lkrshp  39677  lduallvec  39726  dochkr1  42050  dochkr1OLDN  42051  lcfl7lem  42071  lclkrlem2m  42091  lclkrlem2o  42093  lclkrlem2p  42094  lcfrlem1  42114  lcfrlem2  42115  lcfrlem3  42116  lcfrlem29  42143  lcfrlem31  42145  lcfrlem33  42147  mapdpglem17N  42260  mapdpglem18  42261  mapdpglem19  42262  mapdpglem21  42264  mapdpglem22  42265  hdmapip1  42488  hgmapvvlem1  42495  hgmapvvlem2  42496  hgmapvvlem3  42497  prjspersym  43137  lincreslvec3  49052  isldepslvec2  49055