Theorem lvecdrng 21381

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  Scalarcsca 17432  DivRingcdr 20981  LModclmod 21136  LVecclvec 21378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-lvec 21379

This theorem is used by:  lsslvec  21385  lvecvs0or  21387  lssvs0or  21389  lvecinv  21392  lspsnvs  21393  lspsneq  21401  lspfixed  21407  lspexch  21408  lspsolv  21422  islbs2  21433  islbs3  21434  obsne0  22032  islinds4  22142  nvctvc  25020  lssnvc  25022  cvsunit  25453  cvsdivcl  25455  cphsubrg  25502  cphreccl  25503  cphqss  25510  phclm  25554  ipcau2  25556  tcphcph  25559  hlprlem  25689  ishl2  25692  quslvec  33964  0nellinds  33969  lmhmlvec2  34294  dimlssid  34307  lfl1  40203  lkrsc  40230  eqlkr3  40234  lkrlsp  40235  lkrshp  40238  lduallvec  40287  dochkr1  42611  dochkr1OLDN  42612  lcfl7lem  42632  lclkrlem2m  42652  lclkrlem2o  42654  lclkrlem2p  42655  lcfrlem1  42675  lcfrlem2  42676  lcfrlem3  42677  lcfrlem29  42704  lcfrlem31  42706  lcfrlem33  42708  mapdpglem17N  42821  mapdpglem18  42822  mapdpglem19  42823  mapdpglem21  42825  mapdpglem22  42826  hdmapip1  43049  hgmapvvlem1  43056  hgmapvvlem2  43057  hgmapvvlem3  43058  prjspersym  43711  lincreslvec3  49670  isldepslvec2  49673