Theorem lvecdrng 21049

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  Scalarcsca 17174  DivRingcdr 20654  LModclmod 20803  LVecclvec 21046

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-lvec 21047

This theorem is referenced by:  lsslvec  21053  lvecvs0or  21055  lssvs0or  21057  lvecinv  21060  lspsnvs  21061  lspsneq  21069  lspfixed  21075  lspexch  21076  lspsolv  21090  islbs2  21101  islbs3  21102  obsne0  21672  islinds4  21782  nvctvc  24625  lssnvc  24627  cvsunit  25068  cvsdivcl  25070  cphsubrg  25117  cphreccl  25118  cphqss  25125  phclm  25169  ipcau2  25171  tcphcph  25174  hlprlem  25304  ishl2  25307  quslvec  33336  0nellinds  33346  lmhmlvec2  33643  dimlssid  33656  lfl1  39179  lkrsc  39206  eqlkr3  39210  lkrlsp  39211  lkrshp  39214  lduallvec  39263  dochkr1  41587  dochkr1OLDN  41588  lcfl7lem  41608  lclkrlem2m  41628  lclkrlem2o  41630  lclkrlem2p  41631  lcfrlem1  41651  lcfrlem2  41652  lcfrlem3  41653  lcfrlem29  41680  lcfrlem31  41682  lcfrlem33  41684  mapdpglem17N  41797  mapdpglem18  41798  mapdpglem19  41799  mapdpglem21  41801  mapdpglem22  41802  hdmapip1  42025  hgmapvvlem1  42032  hgmapvvlem2  42033  hgmapvvlem3  42034  prjspersym  42715  lincreslvec3  48597  isldepslvec2  48600