Theorem lvecdrng 21090

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  Scalarcsca 17212  DivRingcdr 20695  LModclmod 20844  LVecclvec 21087

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 6446  df-fv 6498  df-lvec 21088

This theorem is referenced by:  lsslvec  21094  lvecvs0or  21096  lssvs0or  21098  lvecinv  21101  lspsnvs  21102  lspsneq  21110  lspfixed  21116  lspexch  21117  lspsolv  21131  islbs2  21142  islbs3  21143  obsne0  21713  islinds4  21823  nvctvc  24674  lssnvc  24676  cvsunit  25107  cvsdivcl  25109  cphsubrg  25156  cphreccl  25157  cphqss  25164  phclm  25208  ipcau2  25210  tcphcph  25213  hlprlem  25343  ishl2  25346  quslvec  33440  0nellinds  33450  lmhmlvec2  33784  dimlssid  33797  lfl1  39527  lkrsc  39554  eqlkr3  39558  lkrlsp  39559  lkrshp  39562  lduallvec  39611  dochkr1  41935  dochkr1OLDN  41936  lcfl7lem  41956  lclkrlem2m  41976  lclkrlem2o  41978  lclkrlem2p  41979  lcfrlem1  41999  lcfrlem2  42000  lcfrlem3  42001  lcfrlem29  42028  lcfrlem31  42030  lcfrlem33  42032  mapdpglem17N  42145  mapdpglem18  42146  mapdpglem19  42147  mapdpglem21  42149  mapdpglem22  42150  hdmapip1  42373  hgmapvvlem1  42380  hgmapvvlem2  42381  hgmapvvlem3  42382  prjspersym  43051  lincreslvec3  48955  isldepslvec2  48958