Theorem lvecdrng 19318

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

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145  ‘cfv 6030  Scalarcsca 16152  DivRingcdr 18957  LModclmod 19073  LVecclvec 19315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-lvec 19316

This theorem is referenced by:  lsslvec  19320  lvecvs0or  19321  lssvs0or  19323  lvecinv  19326  lspsnvs  19327  lspsneq  19335  lspfixed  19341  lspfixedOLD  19342  lspexch  19343  lspsolv  19357  islbs2  19369  islbs3  19370  obsne0  20286  islinds4  20391  nvctvc  22724  lssnvc  22726  cvsunit  23150  cvsdivcl  23152  cphsubrg  23199  cphreccl  23200  cphqss  23207  tchclm  23250  ipcau2  23252  tchcph  23255  hlprlem  23382  ishl2  23385  lfl1  34879  lkrsc  34906  eqlkr3  34910  lkrlsp  34911  lkrshp  34914  lduallvec  34963  dochkr1  37288  dochkr1OLDN  37289  lcfl7lem  37309  lclkrlem2m  37329  lclkrlem2o  37331  lclkrlem2p  37332  lcfrlem1  37352  lcfrlem2  37353  lcfrlem3  37354  lcfrlem29  37381  lcfrlem31  37383  lcfrlem33  37385  mapdpglem17N  37498  mapdpglem18  37499  mapdpglem19  37500  mapdpglem21  37502  mapdpglem22  37503  hdmapip1  37726  hgmapvvlem1  37733  hgmapvvlem2  37734  hgmapvvlem3  37735  lincreslvec3  42796  isldepslvec2  42799