Theorem lveclmod 21062

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 2735	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2	1	islvec 21060	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
3	2	simplbi 497	1 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6530  Scalarcsca 17272  DivRingcdr 20687  LModclmod 20815  LVecclvec 21058

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-lvec 21059

This theorem is referenced by:  lveclmodd  21063  lsslvec  21065  lvecvs0or  21067  lssvs0or  21069  lvecvscan  21070  lvecvscan2  21071  lvecinv  21072  lspsnvs  21073  lspsneleq  21074  lspsncmp  21075  lspsnne1  21076  lspsnnecom  21078  lspabs2  21079  lspabs3  21080  lspsneq  21081  ellspsn4  21083  lspdisj  21084  lspdisjb  21085  lspdisj2  21086  lspfixed  21087  lspexch  21088  lspexchn1  21089  lspindpi  21091  lvecindp  21097  lvecindp2  21098  lsmcv  21100  lspsolv  21102  lssacsex  21103  lspsnat  21104  lsppratlem2  21107  lsppratlem3  21108  lsppratlem4  21109  lsppratlem6  21111  lspprat  21112  islbs2  21113  islbs3  21114  lbsacsbs  21115  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  phllmod  21588  isphld  21612  islinds4  21793  lvecisfrlm  21801  cvsi  25079  0nellinds  33331  lindssn  33339  linds2eq  33342  exsslsb  33582  lvecdim0i  33591  lssdimle  33593  tngdim  33599  matdim  33601  lbslsat  33602  lsatdim  33603  drngdimgt0  33604  lindsunlem  33610  lindsun  33611  lbsdiflsp0  33612  dimkerim  33613  qusdimsum  33614  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  extdg1id  33653  ccfldextdgrr  33659  lindsadd  37583  lshpnelb  38948  lshpnel2N  38949  lshpdisj  38951  lshpcmp  38952  lsatcmp  38967  lsatcmp2  38968  lsatel  38969  lsatelbN  38970  lsatfixedN  38973  lsmcv2  38993  lsatcv0  38995  lsatcveq0  38996  lsat0cv  38997  lcvp  39004  lcv1  39005  lcv2  39006  lsatexch  39007  lsatnem0  39009  lsatexch1  39010  lsatcv0eq  39011  lsatcv1  39012  lsatcvatlem  39013  lsatcvat  39014  lsatcvat2  39015  lsatcvat3  39016  islshpcv  39017  l1cvpat  39018  l1cvat  39019  lfl1  39034  lkrsc  39061  lkrscss  39062  eqlkr  39063  eqlkr3  39065  lkrlsp  39066  lkrlsp3  39068  lkrshp  39069  lkrshp3  39070  lkrshpor  39071  lkrshp4  39072  lshpsmreu  39073  lshpkrlem1  39074  lshpkrlem4  39077  lshpkrlem5  39078  lshpkrlem6  39079  lshpkr  39081  lshpkrex  39082  lfl1dim  39085  lfl1dim2N  39086  lduallvec  39118  lduallkr3  39126  lkrpssN  39127  ldual1dim  39130  lkrss2N  39133  lkreqN  39134  lkrlspeqN  39135  dva0g  40992  dia1dim2  41027  dia1dimid  41028  dia2dimlem5  41033  dia2dimlem7  41035  dia2dimlem9  41037  dia2dimlem10  41038  dia2dimlem13  41041  dvhlmod  41075  diblsmopel  41136  lclkrlem2m  41484  lclkrlem2n  41485  lcfrlem1  41507  lcfrlem2  41508  lcfrlem3  41509  lcdlmod  41557  baerlem3lem1  41672  baerlem5alem1  41673  baerlem5blem1  41674  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdindp0  41684  mapdindp1  41685  mapdindp2  41686  mapdindp3  41687  mapdindp4  41688  lspindp5  41735  lvecgrp  42507  lvecring  42508  prjspersym  42577  prjsper  42578  prjspreln0  42579  prjspvs  42580  prjspeclsp  42582  0prjspn  42598  lincreslvec3  48406  isldepslvec2  48409  lindssnlvec  48410  lvecpsslmod  48431