Theorem lvecdrng 21127

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Scalarcsca 17314  DivRingcdr 20751  LModclmod 20880  LVecclvec 21124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-lvec 21125

This theorem is referenced by:  lsslvec  21131  lvecvs0or  21133  lssvs0or  21135  lvecinv  21138  lspsnvs  21139  lspsneq  21147  lspfixed  21153  lspexch  21154  lspsolv  21168  islbs2  21179  islbs3  21180  obsne0  21768  islinds4  21878  nvctvc  24742  lssnvc  24744  cvsunit  25183  cvsdivcl  25185  cphsubrg  25233  cphreccl  25234  cphqss  25241  phclm  25285  ipcau2  25287  tcphcph  25290  hlprlem  25420  ishl2  25423  quslvec  33353  0nellinds  33363  lmhmlvec2  33632  dimlssid  33645  lfl1  39026  lkrsc  39053  eqlkr3  39057  lkrlsp  39058  lkrshp  39061  lduallvec  39110  dochkr1  41435  dochkr1OLDN  41436  lcfl7lem  41456  lclkrlem2m  41476  lclkrlem2o  41478  lclkrlem2p  41479  lcfrlem1  41499  lcfrlem2  41500  lcfrlem3  41501  lcfrlem29  41528  lcfrlem31  41530  lcfrlem33  41532  mapdpglem17N  41645  mapdpglem18  41646  mapdpglem19  41647  mapdpglem21  41649  mapdpglem22  41650  hdmapip1  41873  hgmapvvlem1  41880  hgmapvvlem2  41881  hgmapvvlem3  41882  prjspersym  42562  lincreslvec3  48211  isldepslvec2  48214