Theorem lvecdrng 21069

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  Scalarcsca 17192  DivRingcdr 20674  LModclmod 20823  LVecclvec 21066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-lvec 21067

This theorem is referenced by:  lsslvec  21073  lvecvs0or  21075  lssvs0or  21077  lvecinv  21080  lspsnvs  21081  lspsneq  21089  lspfixed  21095  lspexch  21096  lspsolv  21110  islbs2  21121  islbs3  21122  obsne0  21692  islinds4  21802  nvctvc  24656  lssnvc  24658  cvsunit  25099  cvsdivcl  25101  cphsubrg  25148  cphreccl  25149  cphqss  25156  phclm  25200  ipcau2  25202  tcphcph  25205  hlprlem  25335  ishl2  25338  quslvec  33452  0nellinds  33462  lmhmlvec2  33796  dimlssid  33809  lfl1  39435  lkrsc  39462  eqlkr3  39466  lkrlsp  39467  lkrshp  39470  lduallvec  39519  dochkr1  41843  dochkr1OLDN  41844  lcfl7lem  41864  lclkrlem2m  41884  lclkrlem2o  41886  lclkrlem2p  41887  lcfrlem1  41907  lcfrlem2  41908  lcfrlem3  41909  lcfrlem29  41936  lcfrlem31  41938  lcfrlem33  41940  mapdpglem17N  42053  mapdpglem18  42054  mapdpglem19  42055  mapdpglem21  42057  mapdpglem22  42058  hdmapip1  42281  hgmapvvlem1  42288  hgmapvvlem2  42289  hgmapvvlem3  42290  prjspersym  42954  lincreslvec3  48831  isldepslvec2  48834