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

Theorem lvecdrng 16182
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 16181 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  F  e.  DivRing ) )
32simprbi 452 1  |-  ( W  e.  LVec  ->  F  e.  DivRing )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   ` cfv 5457  Scalarcsca 13537   DivRingcdr 15840   LModclmod 15955   LVecclvec 16179
This theorem is referenced by:  lsslvec  16184  lvecvs0or  16185  lssvs0or  16187  lvecinv  16190  lspsnvs  16191  lspsneq  16199  lspfixed  16205  lspexch  16206  lspsolv  16220  islbs2  16231  islbs3  16232  obsne0  16957  nvctvc  18740  lssnvc  18742  cphsubrg  19148  cphreccl  19149  cphqss  19156  tchclm  19194  ipcau2  19196  tchcph  19199  hlprlem  19326  ishl2  19329  sitgclbn  24662  islinds4  27296  lfl1  29942  lkrsc  29969  eqlkr3  29973  lkrlsp  29974  lkrshp  29977  lduallvec  30026  dochkr1  32350  dochkr1OLDN  32351  lcfl7lem  32371  lclkrlem2m  32391  lclkrlem2o  32393  lclkrlem2p  32394  lcfrlem1  32414  lcfrlem2  32415  lcfrlem3  32416  lcfrlem29  32443  lcfrlem31  32445  lcfrlem33  32447  mapdpglem17N  32560  mapdpglem18  32561  mapdpglem19  32562  mapdpglem21  32564  mapdpglem22  32565  hdmapip1  32791  hgmapvvlem1  32798  hgmapvvlem2  32799  hgmapvvlem3  32800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-lvec 16180
  Copyright terms: Public domain W3C validator