Theorem lvecdrng 21293

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Scalarcsca 17349  DivRingcdr 20894  LModclmod 21048  LVecclvec 21290

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-lvec 21291

This theorem is used by:  lsslvec  21297  lvecvs0or  21299  lssvs0or  21301  lvecinv  21304  lspsnvs  21305  lspsneq  21313  lspfixed  21319  lspexch  21320  lspsolv  21334  islbs2  21345  islbs3  21346  obsne0  21942  islinds4  22052  nvctvc  24930  lssnvc  24932  cvsunit  25363  cvsdivcl  25365  cphsubrg  25412  cphreccl  25413  cphqss  25420  phclm  25464  ipcau2  25466  tcphcph  25469  hlprlem  25599  ishl2  25602  quslvec  33802  0nellinds  33807  lmhmlvec2  34131  dimlssid  34144  lfl1  39945  lkrsc  39972  eqlkr3  39976  lkrlsp  39977  lkrshp  39980  lduallvec  40029  dochkr1  42353  dochkr1OLDN  42354  lcfl7lem  42374  lclkrlem2m  42394  lclkrlem2o  42396  lclkrlem2p  42397  lcfrlem1  42417  lcfrlem2  42418  lcfrlem3  42419  lcfrlem29  42446  lcfrlem31  42448  lcfrlem33  42450  mapdpglem17N  42563  mapdpglem18  42564  mapdpglem19  42565  mapdpglem21  42567  mapdpglem22  42568  hdmapip1  42791  hgmapvvlem1  42798  hgmapvvlem2  42799  hgmapvvlem3  42800  prjspersym  43455  lincreslvec3  49414  isldepslvec2  49417