Theorem lvecdrng 19465

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

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  ‘cfv 6124  Scalarcsca 16309  DivRingcdr 19104  LModclmod 19220  LVecclvec 19462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-lvec 19463

This theorem is referenced by:  lsslvec  19467  lvecvs0or  19468  lssvs0or  19470  lvecinv  19473  lspsnvs  19474  lspsneq  19482  lspfixed  19488  lspfixedOLD  19489  lspexch  19490  lspsolv  19504  islbs2  19516  islbs3  19517  obsne0  20433  islinds4  20542  nvctvc  22875  lssnvc  22877  cvsunit  23301  cvsdivcl  23303  cphsubrg  23350  cphreccl  23351  cphqss  23358  phclm  23401  ipcau2  23403  tcphcph  23406  hlprlem  23536  ishl2  23539  lfl1  35146  lkrsc  35173  eqlkr3  35177  lkrlsp  35178  lkrshp  35181  lduallvec  35230  dochkr1  37554  dochkr1OLDN  37555  lcfl7lem  37575  lclkrlem2m  37595  lclkrlem2o  37597  lclkrlem2p  37598  lcfrlem1  37618  lcfrlem2  37619  lcfrlem3  37620  lcfrlem29  37647  lcfrlem31  37649  lcfrlem33  37651  mapdpglem17N  37764  mapdpglem18  37765  mapdpglem19  37766  mapdpglem21  37768  mapdpglem22  37769  hdmapip1  37992  hgmapvvlem1  37999  hgmapvvlem2  38000  hgmapvvlem3  38001  lincreslvec3  43119  isldepslvec2  43122