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

Theorem lvecdrng 19850
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 19849 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 499 1 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2114  cfv 6329  Scalarcsca 16544  DivRingcdr 19475  LModclmod 19607  LVecclvec 19847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-nul 4268  df-if 4442  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4813  df-br 5041  df-iota 6288  df-fv 6337  df-lvec 19848
This theorem is referenced by:  lsslvec  19852  lvecvs0or  19853  lssvs0or  19855  lvecinv  19858  lspsnvs  19859  lspsneq  19867  lspfixed  19873  lspexch  19874  lspsolv  19888  islbs2  19899  islbs3  19900  obsne0  20842  islinds4  20952  nvctvc  23282  lssnvc  23284  cvsunit  23712  cvsdivcl  23714  cphsubrg  23761  cphreccl  23762  cphqss  23769  phclm  23812  ipcau2  23814  tcphcph  23817  hlprlem  23947  ishl2  23950  0nellinds  30940  lmhmlvec2  31025  lfl1  36239  lkrsc  36266  eqlkr3  36270  lkrlsp  36271  lkrshp  36274  lduallvec  36323  dochkr1  38647  dochkr1OLDN  38648  lcfl7lem  38668  lclkrlem2m  38688  lclkrlem2o  38690  lclkrlem2p  38691  lcfrlem1  38711  lcfrlem2  38712  lcfrlem3  38713  lcfrlem29  38740  lcfrlem31  38742  lcfrlem33  38744  mapdpglem17N  38857  mapdpglem18  38858  mapdpglem19  38859  mapdpglem21  38861  mapdpglem22  38862  hdmapip1  39085  hgmapvvlem1  39092  hgmapvvlem2  39093  hgmapvvlem3  39094  prjspersym  39381  lincreslvec3  44667  isldepslvec2  44670
  Copyright terms: Public domain W3C validator