Theorem lvecdrng 21027

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  Scalarcsca 17182  DivRingcdr 20632  LModclmod 20781  LVecclvec 21024

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-lvec 21025

This theorem is referenced by:  lsslvec  21031  lvecvs0or  21033  lssvs0or  21035  lvecinv  21038  lspsnvs  21039  lspsneq  21047  lspfixed  21053  lspexch  21054  lspsolv  21068  islbs2  21079  islbs3  21080  obsne0  21650  islinds4  21760  nvctvc  24604  lssnvc  24606  cvsunit  25047  cvsdivcl  25049  cphsubrg  25096  cphreccl  25097  cphqss  25104  phclm  25148  ipcau2  25150  tcphcph  25153  hlprlem  25283  ishl2  25286  quslvec  33307  0nellinds  33317  lmhmlvec2  33591  dimlssid  33604  lfl1  39048  lkrsc  39075  eqlkr3  39079  lkrlsp  39080  lkrshp  39083  lduallvec  39132  dochkr1  41457  dochkr1OLDN  41458  lcfl7lem  41478  lclkrlem2m  41498  lclkrlem2o  41500  lclkrlem2p  41501  lcfrlem1  41521  lcfrlem2  41522  lcfrlem3  41523  lcfrlem29  41550  lcfrlem31  41552  lcfrlem33  41554  mapdpglem17N  41667  mapdpglem18  41668  mapdpglem19  41669  mapdpglem21  41671  mapdpglem22  41672  hdmapip1  41895  hgmapvvlem1  41902  hgmapvvlem2  41903  hgmapvvlem3  41904  prjspersym  42580  lincreslvec3  48455  isldepslvec2  48458