MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lveclmod Unicode version

Theorem lveclmod 15859
Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)
Assertion
Ref Expression
lveclmod  |-  ( W  e.  LVec  ->  W  e. 
LMod )

Proof of Theorem lveclmod
StepHypRef Expression
1 eqid 2283 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 15857 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 446 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   ` cfv 5255  Scalarcsca 13211   DivRingcdr 15512   LModclmod 15627   LVecclvec 15855
This theorem is referenced by:  lsslvec  15860  lvecvs0or  15861  lssvs0or  15863  lvecvscan  15864  lvecvscan2  15865  lvecinv  15866  lspsnvs  15867  lspsneleq  15868  lspsncmp  15869  lspsnne1  15870  lspsnnecom  15872  lspabs2  15873  lspabs3  15874  lspsneq  15875  lspsnel4  15877  lspdisj  15878  lspdisjb  15879  lspdisj2  15880  lspfixed  15881  lspexch  15882  lspexchn1  15883  lspindpi  15885  lvecindp  15891  lvecindp2  15892  lsmcv  15894  lspsolv  15896  lssacsex  15897  lspsnat  15898  lsppratlem2  15901  lsppratlem3  15902  lsppratlem4  15903  lsppratlem6  15905  lspprat  15906  islbs2  15907  islbs3  15908  lbsacsbs  15909  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  phllmod  16534  isphld  16558  islinds4  27305  lshpnelb  29174  lshpnel2N  29175  lshpdisj  29177  lshpcmp  29178  lsatcmp  29193  lsatcmp2  29194  lsatel  29195  lsatelbN  29196  lsatfixedN  29199  lsmcv2  29219  lsatcv0  29221  lsatcveq0  29222  lsat0cv  29223  lcvp  29230  lcv1  29231  lcv2  29232  lsatexch  29233  lsatnem0  29235  lsatexch1  29236  lsatcv0eq  29237  lsatcv1  29238  lsatcvatlem  29239  lsatcvat  29240  lsatcvat2  29241  lsatcvat3  29242  islshpcv  29243  l1cvpat  29244  l1cvat  29245  lfl1  29260  lkrsc  29287  lkrscss  29288  eqlkr  29289  eqlkr3  29291  lkrlsp  29292  lkrlsp3  29294  lkrshp  29295  lkrshp3  29296  lkrshpor  29297  lkrshp4  29298  lshpsmreu  29299  lshpkrlem1  29300  lshpkrlem4  29303  lshpkrlem5  29304  lshpkrlem6  29305  lshpkr  29307  lshpkrex  29308  lfl1dim  29311  lfl1dim2N  29312  lduallvec  29344  lduallkr3  29352  lkrpssN  29353  ldual1dim  29356  lkrss2N  29359  lkreqN  29360  lkrlspeqN  29361  dva0g  31217  dia1dim2  31252  dia1dimid  31253  dia2dimlem5  31258  dia2dimlem7  31260  dia2dimlem9  31262  dia2dimlem10  31263  dia2dimlem13  31266  dvhlmod  31300  diblsmopel  31361  lclkrlem2m  31709  lclkrlem2n  31710  lcfrlem1  31732  lcfrlem2  31733  lcfrlem3  31734  lcdlmod  31782  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdindp0  31909  mapdindp1  31910  mapdindp2  31911  mapdindp3  31912  mapdindp4  31913  lspindp5  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-lvec 15856
  Copyright terms: Public domain W3C validator