Theorem lveclmod 21382

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

This proof depends on syntax axioms:   → wi 4   ∈ 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:  lveclmodd  21383  lsslvec  21385  lvecvs0or  21387  lssvs0or  21389  lvecvscan  21390  lvecvscan2  21391  lvecinv  21392  lspsnvs  21393  lspsneleq  21394  lspsncmp  21395  lspsnne1  21396  lspsnnecom  21398  lspabs2  21399  lspabs3  21400  lspsneq  21401  ellspsn4  21403  lspdisj  21404  lspdisjb  21405  lspdisj2  21406  lspfixed  21407  lspexch  21408  lspexchn1  21409  lspindpi  21411  lvecindp  21417  lvecindp2  21418  lsmcv  21420  lspsolv  21422  lssacsex  21423  lspsnat  21424  lsppratlem2  21427  lsppratlem3  21428  lsppratlem4  21429  lsppratlem6  21431  lspprat  21432  islbs2  21433  islbs3  21434  lbsacsbs  21435  lbsextlem2  21438  lbsextlem3  21439  lbsextlem4  21440  phllmod  21937  isphld  21961  islinds4  22142  lvecisfrlm  22150  cvsi  25452  0nellinds  33969  lindssn  33976  linds2eq  33979  exsslsb  34272  lvecdim0i  34281  lssdimle  34283  tngdim  34288  matdim  34290  lbslsat  34291  lsatdim  34292  drngdimgt0  34293  lindsunlem  34299  lindsun  34300  lbsdiflsp0  34301  dimkerim  34302  qusdimsum  34303  fedgmullem1  34304  fedgmullem2  34305  fedgmul  34306  extdg1id  34341  ccfldextdgrr  34347  lindsadd  38612  lshpnelb  40117  lshpnel2N  40118  lshpdisj  40120  lshpcmp  40121  lsatcmp  40136  lsatcmp2  40137  lsatel  40138  lsatelbN  40139  lsatfixedN  40142  lsmcv2  40162  lsatcv0  40164  lsatcveq0  40165  lsat0cv  40166  lcvp  40173  lcv1  40174  lcv2  40175  lsatexch  40176  lsatnem0  40178  lsatexch1  40179  lsatcv0eq  40180  lsatcv1  40181  lsatcvatlem  40182  lsatcvat  40183  lsatcvat2  40184  lsatcvat3  40185  islshpcv  40186  l1cvpat  40187  l1cvat  40188  lfl1  40203  lkrsc  40230  lkrscss  40231  eqlkr  40232  eqlkr3  40234  lkrlsp  40235  lkrlsp3  40237  lkrshp  40238  lkrshp3  40239  lkrshpor  40240  lkrshp4  40241  lshpsmreu  40242  lshpkrlem1  40243  lshpkrlem4  40246  lshpkrlem5  40247  lshpkrlem6  40248  lshpkr  40250  lshpkrex  40251  lfl1dim  40254  lfl1dim2N  40255  lduallvec  40287  lduallkr3  40295  lkrpssN  40296  ldual1dim  40299  lkrss2N  40302  lkreqN  40303  lkrlspeqN  40304  dva0g  42160  dia1dim2  42195  dia1dimid  42196  dia2dimlem5  42201  dia2dimlem7  42203  dia2dimlem9  42205  dia2dimlem10  42206  dia2dimlem13  42209  dvhlmod  42243  diblsmopel  42304  lclkrlem2m  42652  lclkrlem2n  42653  lcfrlem1  42675  lcfrlem2  42676  lcfrlem3  42677  lcdlmod  42725  baerlem3lem1  42840  baerlem5alem1  42841  baerlem5blem1  42842  baerlem3lem2  42843  baerlem5alem2  42844  baerlem5blem2  42845  baerlem5amN  42849  baerlem5bmN  42850  baerlem5abmN  42851  mapdindp0  42852  mapdindp1  42853  mapdindp2  42854  mapdindp3  42855  mapdindp4  42856  lspindp5  42903  lvecgrp  43677  lvecring  43678  prjspersym  43711  prjsper  43712  prjspreln0  43713  prjspvs  43714  prjspeclsp  43716  lincreslvec3  49670  isldepslvec2  49673  lindssnlvec  49674  lvecpsslmod  49695