Theorem lvecdrng 21380

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  Scalarcsca 17431  DivRingcdr 20980  LModclmod 21135  LVecclvec 21377

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-lvec 21378

This theorem is used by:  lsslvec  21384  lvecvs0or  21386  lssvs0or  21388  lvecinv  21391  lspsnvs  21392  lspsneq  21400  lspfixed  21406  lspexch  21407  lspsolv  21421  islbs2  21432  islbs3  21433  obsne0  22031  islinds4  22141  nvctvc  25019  lssnvc  25021  cvsunit  25452  cvsdivcl  25454  cphsubrg  25501  cphreccl  25502  cphqss  25509  phclm  25553  ipcau2  25555  tcphcph  25558  hlprlem  25688  ishl2  25691  quslvec  33921  0nellinds  33926  lmhmlvec2  34251  dimlssid  34264  lfl1  40127  lkrsc  40154  eqlkr3  40158  lkrlsp  40159  lkrshp  40162  lduallvec  40211  dochkr1  42535  dochkr1OLDN  42536  lcfl7lem  42556  lclkrlem2m  42576  lclkrlem2o  42578  lclkrlem2p  42579  lcfrlem1  42599  lcfrlem2  42600  lcfrlem3  42601  lcfrlem29  42628  lcfrlem31  42630  lcfrlem33  42632  mapdpglem17N  42745  mapdpglem18  42746  mapdpglem19  42747  mapdpglem21  42749  mapdpglem22  42750  hdmapip1  42973  hgmapvvlem1  42980  hgmapvvlem2  42981  hgmapvvlem3  42982  prjspersym  43635  lincreslvec3  49593  isldepslvec2  49596