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

Theorem lvecdrng 19033
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 19032 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 480 1 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  cfv 5852  Scalarcsca 15872  DivRingcdr 18675  LModclmod 18791  LVecclvec 19030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-lvec 19031
This theorem is referenced by:  lsslvec  19035  lvecvs0or  19036  lssvs0or  19038  lvecinv  19041  lspsnvs  19042  lspsneq  19050  lspfixed  19056  lspexch  19057  lspsolv  19071  islbs2  19082  islbs3  19083  obsne0  19997  islinds4  20102  nvctvc  22423  lssnvc  22425  cvsunit  22850  cvsdivcl  22852  cphsubrg  22899  cphreccl  22900  cphqss  22907  tchclm  22950  ipcau2  22952  tchcph  22955  hlprlem  23082  ishl2  23085  lfl1  33864  lkrsc  33891  eqlkr3  33895  lkrlsp  33896  lkrshp  33899  lduallvec  33948  dochkr1  36274  dochkr1OLDN  36275  lcfl7lem  36295  lclkrlem2m  36315  lclkrlem2o  36317  lclkrlem2p  36318  lcfrlem1  36338  lcfrlem2  36339  lcfrlem3  36340  lcfrlem29  36367  lcfrlem31  36369  lcfrlem33  36371  mapdpglem17N  36484  mapdpglem18  36485  mapdpglem19  36486  mapdpglem21  36488  mapdpglem22  36489  hdmapip1  36715  hgmapvvlem1  36722  hgmapvvlem2  36723  hgmapvvlem3  36724  lincreslvec3  41580  isldepslvec2  41583
  Copyright terms: Public domain W3C validator