Theorem lvecdrng 21019

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  Scalarcsca 17230  DivRingcdr 20645  LModclmod 20773  LVecclvec 21016

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-lvec 21017

This theorem is referenced by:  lsslvec  21023  lvecvs0or  21025  lssvs0or  21027  lvecinv  21030  lspsnvs  21031  lspsneq  21039  lspfixed  21045  lspexch  21046  lspsolv  21060  islbs2  21071  islbs3  21072  obsne0  21641  islinds4  21751  nvctvc  24595  lssnvc  24597  cvsunit  25038  cvsdivcl  25040  cphsubrg  25087  cphreccl  25088  cphqss  25095  phclm  25139  ipcau2  25141  tcphcph  25144  hlprlem  25274  ishl2  25277  quslvec  33338  0nellinds  33348  lmhmlvec2  33622  dimlssid  33635  lfl1  39070  lkrsc  39097  eqlkr3  39101  lkrlsp  39102  lkrshp  39105  lduallvec  39154  dochkr1  41479  dochkr1OLDN  41480  lcfl7lem  41500  lclkrlem2m  41520  lclkrlem2o  41522  lclkrlem2p  41523  lcfrlem1  41543  lcfrlem2  41544  lcfrlem3  41545  lcfrlem29  41572  lcfrlem31  41574  lcfrlem33  41576  mapdpglem17N  41689  mapdpglem18  41690  mapdpglem19  41691  mapdpglem21  41693  mapdpglem22  41694  hdmapip1  41917  hgmapvvlem1  41924  hgmapvvlem2  41925  hgmapvvlem3  41926  prjspersym  42602  lincreslvec3  48475  isldepslvec2  48478