Theorem lvecdrng 20704

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ‘cfv 6540  Scalarcsca 17196  DivRingcdr 20304  LModclmod 20459  LVecclvec 20701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-lvec 20702

This theorem is referenced by:  lsslvec  20707  lvecvs0or  20709  lssvs0or  20711  lvecinv  20714  lspsnvs  20715  lspsneq  20723  lspfixed  20729  lspexch  20730  lspsolv  20744  islbs2  20755  islbs3  20756  obsne0  21264  islinds4  21374  nvctvc  24199  lssnvc  24201  cvsunit  24629  cvsdivcl  24631  cphsubrg  24679  cphreccl  24680  cphqss  24687  phclm  24731  ipcau2  24733  tcphcph  24736  hlprlem  24866  ishl2  24869  quslvec  32440  0nellinds  32452  lmhmlvec2  32649  lfl1  37878  lkrsc  37905  eqlkr3  37909  lkrlsp  37910  lkrshp  37913  lduallvec  37962  dochkr1  40287  dochkr1OLDN  40288  lcfl7lem  40308  lclkrlem2m  40328  lclkrlem2o  40330  lclkrlem2p  40331  lcfrlem1  40351  lcfrlem2  40352  lcfrlem3  40353  lcfrlem29  40380  lcfrlem31  40382  lcfrlem33  40384  mapdpglem17N  40497  mapdpglem18  40498  mapdpglem19  40499  mapdpglem21  40501  mapdpglem22  40502  hdmapip1  40725  hgmapvvlem1  40732  hgmapvvlem2  40733  hgmapvvlem3  40734  prjspersym  41293  lincreslvec3  47065  isldepslvec2  47068