Theorem lvecdrng 21068

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

Step	Hyp	Ref	Expression
1		islvec.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	islvec 21067	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
3	2	simprbi 496	1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  Scalarcsca 17279  DivRingcdr 20694  LModclmod 20822  LVecclvec 21065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-lvec 21066

This theorem is referenced by:  lsslvec  21072  lvecvs0or  21074  lssvs0or  21076  lvecinv  21079  lspsnvs  21080  lspsneq  21088  lspfixed  21094  lspexch  21095  lspsolv  21109  islbs2  21120  islbs3  21121  obsne0  21690  islinds4  21800  nvctvc  24644  lssnvc  24646  cvsunit  25087  cvsdivcl  25089  cphsubrg  25137  cphreccl  25138  cphqss  25145  phclm  25189  ipcau2  25191  tcphcph  25194  hlprlem  25324  ishl2  25327  quslvec  33380  0nellinds  33390  lmhmlvec2  33664  dimlssid  33677  lfl1  39093  lkrsc  39120  eqlkr3  39124  lkrlsp  39125  lkrshp  39128  lduallvec  39177  dochkr1  41502  dochkr1OLDN  41503  lcfl7lem  41523  lclkrlem2m  41543  lclkrlem2o  41545  lclkrlem2p  41546  lcfrlem1  41566  lcfrlem2  41567  lcfrlem3  41568  lcfrlem29  41595  lcfrlem31  41597  lcfrlem33  41599  mapdpglem17N  41712  mapdpglem18  41713  mapdpglem19  41714  mapdpglem21  41716  mapdpglem22  41717  hdmapip1  41940  hgmapvvlem1  41947  hgmapvvlem2  41948  hgmapvvlem3  41949  prjspersym  42597  lincreslvec3  48425  isldepslvec2  48428