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

Theorem lvecdrng 15874
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 15873 . 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 1632    e. wcel 1696   ` cfv 5271  Scalarcsca 13227   DivRingcdr 15528   LModclmod 15643   LVecclvec 15871
This theorem is referenced by:  lsslvec  15876  lvecvs0or  15877  lssvs0or  15879  lvecinv  15882  lspsnvs  15883  lspsneq  15891  lspfixed  15897  lspexch  15898  lspsolv  15912  islbs2  15923  islbs3  15924  obsne0  16641  nvctvc  18226  lssnvc  18228  cphsubrg  18632  cphreccl  18633  cphqss  18640  tchclm  18678  ipcau2  18680  tchcph  18683  hlprlem  18800  ishl2  18803  islinds4  27408  lfl1  29882  lkrsc  29909  eqlkr3  29913  lkrlsp  29914  lkrshp  29917  lduallvec  29966  dochkr1  32290  dochkr1OLDN  32291  lcfl7lem  32311  lclkrlem2m  32331  lclkrlem2o  32333  lclkrlem2p  32334  lcfrlem1  32354  lcfrlem2  32355  lcfrlem3  32356  lcfrlem29  32383  lcfrlem31  32385  lcfrlem33  32387  mapdpglem17N  32500  mapdpglem18  32501  mapdpglem19  32502  mapdpglem21  32504  mapdpglem22  32505  hdmapip1  32731  hgmapvvlem1  32738  hgmapvvlem2  32739  hgmapvvlem3  32740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-lvec 15872
  Copyright terms: Public domain W3C validator