MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lvecdrng Unicode version

Theorem lvecdrng 15858
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  |-  F  =  (Scalar `  W )
Assertion
Ref Expression
lvecdrng  |-  ( W  e.  LVec  ->  F  e.  DivRing )

Proof of Theorem lvecdrng
StepHypRef Expression
1 islvec.1 . . 3  |-  F  =  (Scalar `  W )
21islvec 15857 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  F  e.  DivRing ) )
32simprbi 450 1  |-  ( W  e.  LVec  ->  F  e.  DivRing )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   ` cfv 5255  Scalarcsca 13211   DivRingcdr 15512   LModclmod 15627   LVecclvec 15855
This theorem is referenced by:  lsslvec  15860  lvecvs0or  15861  lssvs0or  15863  lvecinv  15866  lspsnvs  15867  lspsneq  15875  lspfixed  15881  lspexch  15882  lspsolv  15896  islbs2  15907  islbs3  15908  obsne0  16625  nvctvc  18210  lssnvc  18212  cphsubrg  18616  cphreccl  18617  cphqss  18624  tchclm  18662  ipcau2  18664  tchcph  18667  hlprlem  18784  ishl2  18787  islinds4  27305  lfl1  29260  lkrsc  29287  eqlkr3  29291  lkrlsp  29292  lkrshp  29295  lduallvec  29344  dochkr1  31668  dochkr1OLDN  31669  lcfl7lem  31689  lclkrlem2m  31709  lclkrlem2o  31711  lclkrlem2p  31712  lcfrlem1  31732  lcfrlem2  31733  lcfrlem3  31734  lcfrlem29  31761  lcfrlem31  31763  lcfrlem33  31765  mapdpglem17N  31878  mapdpglem18  31879  mapdpglem19  31880  mapdpglem21  31882  mapdpglem22  31883  hdmapip1  32109  hgmapvvlem1  32116  hgmapvvlem2  32117  hgmapvvlem3  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-lvec 15856
  Copyright terms: Public domain W3C validator