Theorem lvecdrng 21121

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  Scalarcsca 17300  DivRingcdr 20745  LModclmod 20874  LVecclvec 21118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-lvec 21119

This theorem is referenced by:  lsslvec  21125  lvecvs0or  21127  lssvs0or  21129  lvecinv  21132  lspsnvs  21133  lspsneq  21141  lspfixed  21147  lspexch  21148  lspsolv  21162  islbs2  21173  islbs3  21174  obsne0  21762  islinds4  21872  nvctvc  24736  lssnvc  24738  cvsunit  25177  cvsdivcl  25179  cphsubrg  25227  cphreccl  25228  cphqss  25235  phclm  25279  ipcau2  25281  tcphcph  25284  hlprlem  25414  ishl2  25417  quslvec  33367  0nellinds  33377  lmhmlvec2  33646  dimlssid  33659  lfl1  39051  lkrsc  39078  eqlkr3  39082  lkrlsp  39083  lkrshp  39086  lduallvec  39135  dochkr1  41460  dochkr1OLDN  41461  lcfl7lem  41481  lclkrlem2m  41501  lclkrlem2o  41503  lclkrlem2p  41504  lcfrlem1  41524  lcfrlem2  41525  lcfrlem3  41526  lcfrlem29  41553  lcfrlem31  41555  lcfrlem33  41557  mapdpglem17N  41670  mapdpglem18  41671  mapdpglem19  41672  mapdpglem21  41674  mapdpglem22  41675  hdmapip1  41898  hgmapvvlem1  41905  hgmapvvlem2  41906  hgmapvvlem3  41907  prjspersym  42593  lincreslvec3  48327  isldepslvec2  48330