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

Theorem lvecdrng 20581
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 20580 . 2 (π‘Š ∈ LVec ↔ (π‘Š ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 498 1 (π‘Š ∈ LVec β†’ 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1542   ∈ wcel 2107  β€˜cfv 6497  Scalarcsca 17141  DivRingcdr 20197  LModclmod 20336  LVecclvec 20578
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 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-lvec 20579
This theorem is referenced by:  lsslvec  20584  lvecvs0or  20585  lssvs0or  20587  lvecinv  20590  lspsnvs  20591  lspsneq  20599  lspfixed  20605  lspexch  20606  lspsolv  20620  islbs2  20631  islbs3  20632  obsne0  21147  islinds4  21257  nvctvc  24080  lssnvc  24082  cvsunit  24510  cvsdivcl  24512  cphsubrg  24560  cphreccl  24561  cphqss  24568  phclm  24612  ipcau2  24614  tcphcph  24617  hlprlem  24747  ishl2  24750  0nellinds  32206  lmhmlvec2  32371  lfl1  37578  lkrsc  37605  eqlkr3  37609  lkrlsp  37610  lkrshp  37613  lduallvec  37662  dochkr1  39987  dochkr1OLDN  39988  lcfl7lem  40008  lclkrlem2m  40028  lclkrlem2o  40030  lclkrlem2p  40031  lcfrlem1  40051  lcfrlem2  40052  lcfrlem3  40053  lcfrlem29  40080  lcfrlem31  40082  lcfrlem33  40084  mapdpglem17N  40197  mapdpglem18  40198  mapdpglem19  40199  mapdpglem21  40201  mapdpglem22  40202  hdmapip1  40425  hgmapvvlem1  40432  hgmapvvlem2  40433  hgmapvvlem3  40434  prjspersym  40988  lincreslvec3  46649  isldepslvec2  46652
  Copyright terms: Public domain W3C validator