Theorem lvecdrng 21205

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  Scalarcsca 17312  DivRingcdr 20812  LModclmod 20960  LVecclvec 21202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-lvec 21203

This theorem is referenced by:  lsslvec  21209  lvecvs0or  21211  lssvs0or  21213  lvecinv  21216  lspsnvs  21217  lspsneq  21225  lspfixed  21231  lspexch  21232  lspsolv  21246  islbs2  21257  islbs3  21258  obsne0  21854  islinds4  21964  nvctvc  24836  lssnvc  24838  cvsunit  25269  cvsdivcl  25271  cphsubrg  25318  cphreccl  25319  cphqss  25326  phclm  25370  ipcau2  25372  tcphcph  25375  hlprlem  25505  ishl2  25508  quslvec  33646  0nellinds  33651  lmhmlvec2  33975  dimlssid  33988  lfl1  39812  lkrsc  39839  eqlkr3  39843  lkrlsp  39844  lkrshp  39847  lduallvec  39896  dochkr1  42220  dochkr1OLDN  42221  lcfl7lem  42241  lclkrlem2m  42261  lclkrlem2o  42263  lclkrlem2p  42264  lcfrlem1  42284  lcfrlem2  42285  lcfrlem3  42286  lcfrlem29  42313  lcfrlem31  42315  lcfrlem33  42317  mapdpglem17N  42430  mapdpglem18  42431  mapdpglem19  42432  mapdpglem21  42434  mapdpglem22  42435  hdmapip1  42658  hgmapvvlem1  42665  hgmapvvlem2  42666  hgmapvvlem3  42667  prjspersym  43309  lincreslvec3  49229  isldepslvec2  49232