Theorem lvecdrng 20861

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 20860	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
3	2	simprbi 496	1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ‘cfv 6544  Scalarcsca 17205  DivRingcdr 20501  LModclmod 20615  LVecclvec 20858

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-lvec 20859

This theorem is referenced by:  lsslvec  20865  lvecvs0or  20867  lssvs0or  20869  lvecinv  20872  lspsnvs  20873  lspsneq  20881  lspfixed  20887  lspexch  20888  lspsolv  20902  islbs2  20913  islbs3  20914  obsne0  21500  islinds4  21610  nvctvc  24438  lssnvc  24440  cvsunit  24879  cvsdivcl  24881  cphsubrg  24929  cphreccl  24930  cphqss  24937  phclm  24981  ipcau2  24983  tcphcph  24986  hlprlem  25116  ishl2  25119  quslvec  32742  0nellinds  32754  lmhmlvec2  32989  lfl1  38244  lkrsc  38271  eqlkr3  38275  lkrlsp  38276  lkrshp  38279  lduallvec  38328  dochkr1  40653  dochkr1OLDN  40654  lcfl7lem  40674  lclkrlem2m  40694  lclkrlem2o  40696  lclkrlem2p  40697  lcfrlem1  40717  lcfrlem2  40718  lcfrlem3  40719  lcfrlem29  40746  lcfrlem31  40748  lcfrlem33  40750  mapdpglem17N  40863  mapdpglem18  40864  mapdpglem19  40865  mapdpglem21  40867  mapdpglem22  40868  hdmapip1  41091  hgmapvvlem1  41098  hgmapvvlem2  41099  hgmapvvlem3  41100  prjspersym  41652  lincreslvec3  47252  isldepslvec2  47255