Theorem lvecdrng 21061

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  Scalarcsca 17184  DivRingcdr 20666  LModclmod 20815  LVecclvec 21058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-lvec 21059

This theorem is referenced by:  lsslvec  21065  lvecvs0or  21067  lssvs0or  21069  lvecinv  21072  lspsnvs  21073  lspsneq  21081  lspfixed  21087  lspexch  21088  lspsolv  21102  islbs2  21113  islbs3  21114  obsne0  21684  islinds4  21794  nvctvc  24648  lssnvc  24650  cvsunit  25091  cvsdivcl  25093  cphsubrg  25140  cphreccl  25141  cphqss  25148  phclm  25192  ipcau2  25194  tcphcph  25197  hlprlem  25327  ishl2  25330  quslvec  33422  0nellinds  33432  lmhmlvec2  33757  dimlssid  33770  lfl1  39367  lkrsc  39394  eqlkr3  39398  lkrlsp  39399  lkrshp  39402  lduallvec  39451  dochkr1  41775  dochkr1OLDN  41776  lcfl7lem  41796  lclkrlem2m  41816  lclkrlem2o  41818  lclkrlem2p  41819  lcfrlem1  41839  lcfrlem2  41840  lcfrlem3  41841  lcfrlem29  41868  lcfrlem31  41870  lcfrlem33  41872  mapdpglem17N  41985  mapdpglem18  41986  mapdpglem19  41987  mapdpglem21  41989  mapdpglem22  41990  hdmapip1  42213  hgmapvvlem1  42220  hgmapvvlem2  42221  hgmapvvlem3  42222  prjspersym  42886  lincreslvec3  48764  isldepslvec2  48767