Theorem lvecdrng 20282

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  Scalarcsca 16891  DivRingcdr 19906  LModclmod 20038  LVecclvec 20279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-lvec 20280

This theorem is referenced by:  lsslvec  20284  lvecvs0or  20285  lssvs0or  20287  lvecinv  20290  lspsnvs  20291  lspsneq  20299  lspfixed  20305  lspexch  20306  lspsolv  20320  islbs2  20331  islbs3  20332  obsne0  20842  islinds4  20952  nvctvc  23770  lssnvc  23772  cvsunit  24200  cvsdivcl  24202  cphsubrg  24249  cphreccl  24250  cphqss  24257  phclm  24301  ipcau2  24303  tcphcph  24306  hlprlem  24436  ishl2  24439  0nellinds  31468  lmhmlvec2  31604  lfl1  37011  lkrsc  37038  eqlkr3  37042  lkrlsp  37043  lkrshp  37046  lduallvec  37095  dochkr1  39419  dochkr1OLDN  39420  lcfl7lem  39440  lclkrlem2m  39460  lclkrlem2o  39462  lclkrlem2p  39463  lcfrlem1  39483  lcfrlem2  39484  lcfrlem3  39485  lcfrlem29  39512  lcfrlem31  39514  lcfrlem33  39516  mapdpglem17N  39629  mapdpglem18  39630  mapdpglem19  39631  mapdpglem21  39633  mapdpglem22  39634  hdmapip1  39857  hgmapvvlem1  39864  hgmapvvlem2  39865  hgmapvvlem3  39866  prjspersym  40367  lincreslvec3  45711  isldepslvec2  45714