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

Theorem lvecdrng 20704
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 𝐹 = (Scalar‘𝑊)
Assertion
Ref Expression
lvecdrng (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Proof of Theorem lvecdrng
StepHypRef Expression
1 islvec.1 . . 3 𝐹 = (Scalar‘𝑊)
21islvec 20703 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 498 1 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cfv 6540  Scalarcsca 17196  DivRingcdr 20304  LModclmod 20459  LVecclvec 20701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-lvec 20702
This theorem is referenced by:  lsslvec  20707  lvecvs0or  20709  lssvs0or  20711  lvecinv  20714  lspsnvs  20715  lspsneq  20723  lspfixed  20729  lspexch  20730  lspsolv  20744  islbs2  20755  islbs3  20756  obsne0  21264  islinds4  21374  nvctvc  24199  lssnvc  24201  cvsunit  24629  cvsdivcl  24631  cphsubrg  24679  cphreccl  24680  cphqss  24687  phclm  24731  ipcau2  24733  tcphcph  24736  hlprlem  24866  ishl2  24869  quslvec  32440  0nellinds  32452  lmhmlvec2  32649  lfl1  37878  lkrsc  37905  eqlkr3  37909  lkrlsp  37910  lkrshp  37913  lduallvec  37962  dochkr1  40287  dochkr1OLDN  40288  lcfl7lem  40308  lclkrlem2m  40328  lclkrlem2o  40330  lclkrlem2p  40331  lcfrlem1  40351  lcfrlem2  40352  lcfrlem3  40353  lcfrlem29  40380  lcfrlem31  40382  lcfrlem33  40384  mapdpglem17N  40497  mapdpglem18  40498  mapdpglem19  40499  mapdpglem21  40501  mapdpglem22  40502  hdmapip1  40725  hgmapvvlem1  40732  hgmapvvlem2  40733  hgmapvvlem3  40734  prjspersym  41293  lincreslvec3  47065  isldepslvec2  47068
  Copyright terms: Public domain W3C validator