Theorem lvecdrng 21100

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6499  Scalarcsca 17223  DivRingcdr 20706  LModclmod 20855  LVecclvec 21097

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-lvec 21098

This theorem is referenced by:  lsslvec  21104  lvecvs0or  21106  lssvs0or  21108  lvecinv  21111  lspsnvs  21112  lspsneq  21120  lspfixed  21126  lspexch  21127  lspsolv  21141  islbs2  21152  islbs3  21153  obsne0  21705  islinds4  21815  nvctvc  24665  lssnvc  24667  cvsunit  25098  cvsdivcl  25100  cphsubrg  25147  cphreccl  25148  cphqss  25155  phclm  25199  ipcau2  25201  tcphcph  25204  hlprlem  25334  ishl2  25337  quslvec  33420  0nellinds  33430  lmhmlvec2  33763  dimlssid  33776  lfl1  39516  lkrsc  39543  eqlkr3  39547  lkrlsp  39548  lkrshp  39551  lduallvec  39600  dochkr1  41924  dochkr1OLDN  41925  lcfl7lem  41945  lclkrlem2m  41965  lclkrlem2o  41967  lclkrlem2p  41968  lcfrlem1  41988  lcfrlem2  41989  lcfrlem3  41990  lcfrlem29  42017  lcfrlem31  42019  lcfrlem33  42021  mapdpglem17N  42134  mapdpglem18  42135  mapdpglem19  42136  mapdpglem21  42138  mapdpglem22  42139  hdmapip1  42362  hgmapvvlem1  42369  hgmapvvlem2  42370  hgmapvvlem3  42371  prjspersym  43040  lincreslvec3  48952  isldepslvec2  48955