Theorem lveclmod 21196

Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)

Assertion

Ref	Expression
lveclmod	⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Proof of Theorem lveclmod

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2	1	islvec 21194	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
3	2	simplbi 501	1 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2145  ‘cfv 6525  Scalarcsca 17303  DivRingcdr 20804  LModclmod 20950  LVecclvec 21192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-lvec 21193

This theorem is referenced by:  lveclmodd  21197  lsslvec  21199  lvecvs0or  21201  lssvs0or  21203  lvecvscan  21204  lvecvscan2  21205  lvecinv  21206  lspsnvs  21207  lspsneleq  21208  lspsncmp  21209  lspsnne1  21210  lspsnnecom  21212  lspabs2  21213  lspabs3  21214  lspsneq  21215  ellspsn4  21217  lspdisj  21218  lspdisjb  21219  lspdisj2  21220  lspfixed  21221  lspexch  21222  lspexchn1  21223  lspindpi  21225  lvecindp  21231  lvecindp2  21232  lsmcv  21234  lspsolv  21236  lssacsex  21237  lspsnat  21238  lsppratlem2  21241  lsppratlem3  21242  lsppratlem4  21243  lsppratlem6  21245  lspprat  21246  islbs2  21247  islbs3  21248  lbsacsbs  21249  lbsextlem2  21252  lbsextlem3  21253  lbsextlem4  21254  phllmod  21740  isphld  21764  islinds4  21945  lvecisfrlm  21953  cvsi  25250  0nellinds  33600  lindssn  33607  linds2eq  33610  exsslsb  33904  lvecdim0i  33913  lssdimle  33915  tngdim  33920  matdim  33922  lbslsat  33923  lsatdim  33924  drngdimgt0  33925  lindsunlem  33931  lindsun  33932  lbsdiflsp0  33933  dimkerim  33934  qusdimsum  33935  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  extdg1id  33973  ccfldextdgrr  33979  lindsadd  38124  lshpnelb  39620  lshpnel2N  39621  lshpdisj  39623  lshpcmp  39624  lsatcmp  39639  lsatcmp2  39640  lsatel  39641  lsatelbN  39642  lsatfixedN  39645  lsmcv2  39665  lsatcv0  39667  lsatcveq0  39668  lsat0cv  39669  lcvp  39676  lcv1  39677  lcv2  39678  lsatexch  39679  lsatnem0  39681  lsatexch1  39682  lsatcv0eq  39683  lsatcv1  39684  lsatcvatlem  39685  lsatcvat  39686  lsatcvat2  39687  lsatcvat3  39688  islshpcv  39689  l1cvpat  39690  l1cvat  39691  lfl1  39706  lkrsc  39733  lkrscss  39734  eqlkr  39735  eqlkr3  39737  lkrlsp  39738  lkrlsp3  39740  lkrshp  39741  lkrshp3  39742  lkrshpor  39743  lkrshp4  39744  lshpsmreu  39745  lshpkrlem1  39746  lshpkrlem4  39749  lshpkrlem5  39750  lshpkrlem6  39751  lshpkr  39753  lshpkrex  39754  lfl1dim  39757  lfl1dim2N  39758  lduallvec  39790  lduallkr3  39798  lkrpssN  39799  ldual1dim  39802  lkrss2N  39805  lkreqN  39806  lkrlspeqN  39807  dva0g  41663  dia1dim2  41698  dia1dimid  41699  dia2dimlem5  41704  dia2dimlem7  41706  dia2dimlem9  41708  dia2dimlem10  41709  dia2dimlem13  41712  dvhlmod  41746  diblsmopel  41807  lclkrlem2m  42155  lclkrlem2n  42156  lcfrlem1  42178  lcfrlem2  42179  lcfrlem3  42180  lcdlmod  42228  baerlem3lem1  42343  baerlem5alem1  42344  baerlem5blem1  42345  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  baerlem5amN  42352  baerlem5bmN  42353  baerlem5abmN  42354  mapdindp0  42355  mapdindp1  42356  mapdindp2  42357  mapdindp3  42358  mapdindp4  42359  lspindp5  42406  lvecgrp  43167  lvecring  43168  prjspersym  43201  prjsper  43202  prjspreln0  43203  prjspvs  43204  prjspeclsp  43206  0prjspn  43222  lincreslvec3  49113  isldepslvec2  49116  lindssnlvec  49117  lvecpsslmod  49138