Theorem lvecdrng 21237

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  Scalarcsca 17319  DivRingcdr 20838  LModclmod 20992  LVecclvec 21234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  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 21235

This theorem is used by:  lsslvec  21241  lvecvs0or  21243  lssvs0or  21245  lvecinv  21248  lspsnvs  21249  lspsneq  21257  lspfixed  21263  lspexch  21264  lspsolv  21278  islbs2  21289  islbs3  21290  obsne0  21886  islinds4  21996  nvctvc  24868  lssnvc  24870  cvsunit  25301  cvsdivcl  25303  cphsubrg  25350  cphreccl  25351  cphqss  25358  phclm  25402  ipcau2  25404  tcphcph  25407  hlprlem  25537  ishl2  25540  quslvec  33689  0nellinds  33694  lmhmlvec2  34018  dimlssid  34031  lfl1  39872  lkrsc  39899  eqlkr3  39903  lkrlsp  39904  lkrshp  39907  lduallvec  39956  dochkr1  42280  dochkr1OLDN  42281  lcfl7lem  42301  lclkrlem2m  42321  lclkrlem2o  42323  lclkrlem2p  42324  lcfrlem1  42344  lcfrlem2  42345  lcfrlem3  42346  lcfrlem29  42373  lcfrlem31  42375  lcfrlem33  42377  mapdpglem17N  42490  mapdpglem18  42491  mapdpglem19  42492  mapdpglem21  42494  mapdpglem22  42495  hdmapip1  42718  hgmapvvlem1  42725  hgmapvvlem2  42726  hgmapvvlem3  42727  prjspersym  43367  lincreslvec3  49290  isldepslvec2  49293