Theorem lvecdrng 21104

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  Scalarcsca 17300  DivRingcdr 20729  LModclmod 20858  LVecclvec 21101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-lvec 21102

This theorem is referenced by:  lsslvec  21108  lvecvs0or  21110  lssvs0or  21112  lvecinv  21115  lspsnvs  21116  lspsneq  21124  lspfixed  21130  lspexch  21131  lspsolv  21145  islbs2  21156  islbs3  21157  obsne0  21745  islinds4  21855  nvctvc  24721  lssnvc  24723  cvsunit  25164  cvsdivcl  25166  cphsubrg  25214  cphreccl  25215  cphqss  25222  phclm  25266  ipcau2  25268  tcphcph  25271  hlprlem  25401  ishl2  25404  quslvec  33388  0nellinds  33398  lmhmlvec2  33670  dimlssid  33683  lfl1  39071  lkrsc  39098  eqlkr3  39102  lkrlsp  39103  lkrshp  39106  lduallvec  39155  dochkr1  41480  dochkr1OLDN  41481  lcfl7lem  41501  lclkrlem2m  41521  lclkrlem2o  41523  lclkrlem2p  41524  lcfrlem1  41544  lcfrlem2  41545  lcfrlem3  41546  lcfrlem29  41573  lcfrlem31  41575  lcfrlem33  41577  mapdpglem17N  41690  mapdpglem18  41691  mapdpglem19  41692  mapdpglem21  41694  mapdpglem22  41695  hdmapip1  41918  hgmapvvlem1  41925  hgmapvvlem2  41926  hgmapvvlem3  41927  prjspersym  42617  lincreslvec3  48399  isldepslvec2  48402