Theorem lvecdrng 21102

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  Scalarcsca 17221  DivRingcdr 20708  LModclmod 20857  LVecclvec 21099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-lvec 21100

This theorem is referenced by:  lsslvec  21106  lvecvs0or  21108  lssvs0or  21110  lvecinv  21113  lspsnvs  21114  lspsneq  21122  lspfixed  21128  lspexch  21129  lspsolv  21143  islbs2  21154  islbs3  21155  obsne0  21707  islinds4  21817  nvctvc  24690  lssnvc  24692  cvsunit  25123  cvsdivcl  25125  cphsubrg  25172  cphreccl  25173  cphqss  25180  phclm  25224  ipcau2  25226  tcphcph  25229  hlprlem  25359  ishl2  25362  quslvec  33450  0nellinds  33460  lmhmlvec2  33810  dimlssid  33823  lfl1  39563  lkrsc  39590  eqlkr3  39594  lkrlsp  39595  lkrshp  39598  lduallvec  39647  dochkr1  41971  dochkr1OLDN  41972  lcfl7lem  41992  lclkrlem2m  42012  lclkrlem2o  42014  lclkrlem2p  42015  lcfrlem1  42035  lcfrlem2  42036  lcfrlem3  42037  lcfrlem29  42064  lcfrlem31  42066  lcfrlem33  42068  mapdpglem17N  42181  mapdpglem18  42182  mapdpglem19  42183  mapdpglem21  42185  mapdpglem22  42186  hdmapip1  42409  hgmapvvlem1  42416  hgmapvvlem2  42417  hgmapvvlem3  42418  prjspersym  43058  lincreslvec3  48974  isldepslvec2  48977