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

Theorem lvecdrng 19996
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 19995 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 500 1 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2114  cfv 6339  Scalarcsca 16671  DivRingcdr 19621  LModclmod 19753  LVecclvec 19993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-iota 6297  df-fv 6347  df-lvec 19994
This theorem is referenced by:  lsslvec  19998  lvecvs0or  19999  lssvs0or  20001  lvecinv  20004  lspsnvs  20005  lspsneq  20013  lspfixed  20019  lspexch  20020  lspsolv  20034  islbs2  20045  islbs3  20046  obsne0  20541  islinds4  20651  nvctvc  23453  lssnvc  23455  cvsunit  23883  cvsdivcl  23885  cphsubrg  23932  cphreccl  23933  cphqss  23940  phclm  23984  ipcau2  23986  tcphcph  23989  hlprlem  24119  ishl2  24122  0nellinds  31138  lmhmlvec2  31274  lfl1  36707  lkrsc  36734  eqlkr3  36738  lkrlsp  36739  lkrshp  36742  lduallvec  36791  dochkr1  39115  dochkr1OLDN  39116  lcfl7lem  39136  lclkrlem2m  39156  lclkrlem2o  39158  lclkrlem2p  39159  lcfrlem1  39179  lcfrlem2  39180  lcfrlem3  39181  lcfrlem29  39208  lcfrlem31  39210  lcfrlem33  39212  mapdpglem17N  39325  mapdpglem18  39326  mapdpglem19  39327  mapdpglem21  39329  mapdpglem22  39330  hdmapip1  39553  hgmapvvlem1  39560  hgmapvvlem2  39561  hgmapvvlem3  39562  prjspersym  40023  lincreslvec3  45357  isldepslvec2  45360
  Copyright terms: Public domain W3C validator