Theorem lvecdrng 19879

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ‘cfv 6357  Scalarcsca 16570  DivRingcdr 19504  LModclmod 19636  LVecclvec 19876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-lvec 19877

This theorem is referenced by:  lsslvec  19881  lvecvs0or  19882  lssvs0or  19884  lvecinv  19887  lspsnvs  19888  lspsneq  19896  lspfixed  19902  lspexch  19903  lspsolv  19917  islbs2  19928  islbs3  19929  obsne0  20871  islinds4  20981  nvctvc  23311  lssnvc  23313  cvsunit  23737  cvsdivcl  23739  cphsubrg  23786  cphreccl  23787  cphqss  23794  phclm  23837  ipcau2  23839  tcphcph  23842  hlprlem  23972  ishl2  23975  0nellinds  30937  lmhmlvec2  31019  lfl1  36208  lkrsc  36235  eqlkr3  36239  lkrlsp  36240  lkrshp  36243  lduallvec  36292  dochkr1  38616  dochkr1OLDN  38617  lcfl7lem  38637  lclkrlem2m  38657  lclkrlem2o  38659  lclkrlem2p  38660  lcfrlem1  38680  lcfrlem2  38681  lcfrlem3  38682  lcfrlem29  38709  lcfrlem31  38711  lcfrlem33  38713  mapdpglem17N  38826  mapdpglem18  38827  mapdpglem19  38828  mapdpglem21  38830  mapdpglem22  38831  hdmapip1  39054  hgmapvvlem1  39061  hgmapvvlem2  39062  hgmapvvlem3  39063  prjspersym  39264  lincreslvec3  44544  isldepslvec2  44547