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

Theorem lvecdrng 19318
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 19317 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
32simprbi 484 1 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  cfv 6031  Scalarcsca 16152  DivRingcdr 18957  LModclmod 19073  LVecclvec 19315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-lvec 19316
This theorem is referenced by:  lsslvec  19320  lvecvs0or  19321  lssvs0or  19323  lvecinv  19326  lspsnvs  19327  lspsneq  19335  lspfixed  19341  lspfixedOLD  19342  lspexch  19343  lspsolv  19357  islbs2  19369  islbs3  19370  obsne0  20286  islinds4  20391  nvctvc  22724  lssnvc  22726  cvsunit  23150  cvsdivcl  23152  cphsubrg  23199  cphreccl  23200  cphqss  23207  tchclm  23250  ipcau2  23252  tchcph  23255  hlprlem  23382  ishl2  23385  lfl1  34879  lkrsc  34906  eqlkr3  34910  lkrlsp  34911  lkrshp  34914  lduallvec  34963  dochkr1  37288  dochkr1OLDN  37289  lcfl7lem  37309  lclkrlem2m  37329  lclkrlem2o  37331  lclkrlem2p  37332  lcfrlem1  37352  lcfrlem2  37353  lcfrlem3  37354  lcfrlem29  37381  lcfrlem31  37383  lcfrlem33  37385  mapdpglem17N  37498  mapdpglem18  37499  mapdpglem19  37500  mapdpglem21  37502  mapdpglem22  37503  hdmapip1  37726  hgmapvvlem1  37733  hgmapvvlem2  37734  hgmapvvlem3  37735  lincreslvec3  42799  isldepslvec2  42802
  Copyright terms: Public domain W3C validator