Theorem lvecdrng 21032

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ‘cfv 6477  Scalarcsca 17156  DivRingcdr 20637  LModclmod 20786  LVecclvec 21029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-lvec 21030

This theorem is referenced by:  lsslvec  21036  lvecvs0or  21038  lssvs0or  21040  lvecinv  21043  lspsnvs  21044  lspsneq  21052  lspfixed  21058  lspexch  21059  lspsolv  21073  islbs2  21084  islbs3  21085  obsne0  21655  islinds4  21765  nvctvc  24608  lssnvc  24610  cvsunit  25051  cvsdivcl  25053  cphsubrg  25100  cphreccl  25101  cphqss  25108  phclm  25152  ipcau2  25154  tcphcph  25157  hlprlem  25287  ishl2  25290  quslvec  33315  0nellinds  33325  lmhmlvec2  33622  dimlssid  33635  lfl1  39088  lkrsc  39115  eqlkr3  39119  lkrlsp  39120  lkrshp  39123  lduallvec  39172  dochkr1  41496  dochkr1OLDN  41497  lcfl7lem  41517  lclkrlem2m  41537  lclkrlem2o  41539  lclkrlem2p  41540  lcfrlem1  41560  lcfrlem2  41561  lcfrlem3  41562  lcfrlem29  41589  lcfrlem31  41591  lcfrlem33  41593  mapdpglem17N  41706  mapdpglem18  41707  mapdpglem19  41708  mapdpglem21  41710  mapdpglem22  41711  hdmapip1  41934  hgmapvvlem1  41941  hgmapvvlem2  41942  hgmapvvlem3  41943  prjspersym  42619  lincreslvec3  48493  isldepslvec2  48496