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

Theorem lvecdrng 16104
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 16103 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  F  e.  DivRing ) )
32simprbi 451 1  |-  ( W  e.  LVec  ->  F  e.  DivRing )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   ` cfv 5394  Scalarcsca 13459   DivRingcdr 15762   LModclmod 15877   LVecclvec 16101
This theorem is referenced by:  lsslvec  16106  lvecvs0or  16107  lssvs0or  16109  lvecinv  16112  lspsnvs  16113  lspsneq  16121  lspfixed  16127  lspexch  16128  lspsolv  16142  islbs2  16153  islbs3  16154  obsne0  16875  nvctvc  18606  lssnvc  18608  cphsubrg  19014  cphreccl  19015  cphqss  19022  tchclm  19060  ipcau2  19062  tchcph  19065  hlprlem  19188  ishl2  19191  islinds4  26974  lfl1  29185  lkrsc  29212  eqlkr3  29216  lkrlsp  29217  lkrshp  29220  lduallvec  29269  dochkr1  31593  dochkr1OLDN  31594  lcfl7lem  31614  lclkrlem2m  31634  lclkrlem2o  31636  lclkrlem2p  31637  lcfrlem1  31657  lcfrlem2  31658  lcfrlem3  31659  lcfrlem29  31686  lcfrlem31  31688  lcfrlem33  31690  mapdpglem17N  31803  mapdpglem18  31804  mapdpglem19  31805  mapdpglem21  31807  mapdpglem22  31808  hdmapip1  32034  hgmapvvlem1  32041  hgmapvvlem2  32042  hgmapvvlem3  32043
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-lvec 16102
  Copyright terms: Public domain W3C validator