Theorem lvecdrng 20367

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ‘cfv 6433  Scalarcsca 16965  DivRingcdr 19991  LModclmod 20123  LVecclvec 20364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-lvec 20365

This theorem is referenced by:  lsslvec  20369  lvecvs0or  20370  lssvs0or  20372  lvecinv  20375  lspsnvs  20376  lspsneq  20384  lspfixed  20390  lspexch  20391  lspsolv  20405  islbs2  20416  islbs3  20417  obsne0  20932  islinds4  21042  nvctvc  23864  lssnvc  23866  cvsunit  24294  cvsdivcl  24296  cphsubrg  24344  cphreccl  24345  cphqss  24352  phclm  24396  ipcau2  24398  tcphcph  24401  hlprlem  24531  ishl2  24534  0nellinds  31566  lmhmlvec2  31702  lfl1  37084  lkrsc  37111  eqlkr3  37115  lkrlsp  37116  lkrshp  37119  lduallvec  37168  dochkr1  39492  dochkr1OLDN  39493  lcfl7lem  39513  lclkrlem2m  39533  lclkrlem2o  39535  lclkrlem2p  39536  lcfrlem1  39556  lcfrlem2  39557  lcfrlem3  39558  lcfrlem29  39585  lcfrlem31  39587  lcfrlem33  39589  mapdpglem17N  39702  mapdpglem18  39703  mapdpglem19  39704  mapdpglem21  39706  mapdpglem22  39707  hdmapip1  39930  hgmapvvlem1  39937  hgmapvvlem2  39938  hgmapvvlem3  39939  prjspersym  40446  lincreslvec3  45823  isldepslvec2  45826