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

Theorem lvecdrng 17963
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 17962 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  F  e.  DivRing ) )
32simprbi 462 1  |-  ( W  e.  LVec  ->  F  e.  DivRing )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842   ` cfv 5525  Scalarcsca 14804   DivRingcdr 17608   LModclmod 17724   LVecclvec 17960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5489  df-fv 5533  df-lvec 17961
This theorem is referenced by:  lsslvec  17965  lvecvs0or  17966  lssvs0or  17968  lvecinv  17971  lspsnvs  17972  lspsneq  17980  lspfixed  17986  lspexch  17987  lspsolv  18001  islbs2  18012  islbs3  18013  obsne0  18946  islinds4  19054  nvctvc  21392  lssnvc  21394  cvsunit  21792  cvsdivcl  21794  cphsubrg  21811  cphreccl  21812  cphqss  21819  tchclm  21859  ipcau2  21861  tchcph  21864  hlprlem  21991  ishl2  21994  lfl1  32069  lkrsc  32096  eqlkr3  32100  lkrlsp  32101  lkrshp  32104  lduallvec  32153  dochkr1  34479  dochkr1OLDN  34480  lcfl7lem  34500  lclkrlem2m  34520  lclkrlem2o  34522  lclkrlem2p  34523  lcfrlem1  34543  lcfrlem2  34544  lcfrlem3  34545  lcfrlem29  34572  lcfrlem31  34574  lcfrlem33  34576  mapdpglem17N  34689  mapdpglem18  34690  mapdpglem19  34691  mapdpglem21  34693  mapdpglem22  34694  hdmapip1  34920  hgmapvvlem1  34927  hgmapvvlem2  34928  hgmapvvlem3  34929  lincreslvec3  38574  isldepslvec2  38577
  Copyright terms: Public domain W3C validator