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

Theorem lveclmod 15875
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 2296 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 15873 . 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 1696   ` cfv 5271  Scalarcsca 13227   DivRingcdr 15528   LModclmod 15643   LVecclvec 15871
This theorem is referenced by:  lsslvec  15876  lvecvs0or  15877  lssvs0or  15879  lvecvscan  15880  lvecvscan2  15881  lvecinv  15882  lspsnvs  15883  lspsneleq  15884  lspsncmp  15885  lspsnne1  15886  lspsnnecom  15888  lspabs2  15889  lspabs3  15890  lspsneq  15891  lspsnel4  15893  lspdisj  15894  lspdisjb  15895  lspdisj2  15896  lspfixed  15897  lspexch  15898  lspexchn1  15899  lspindpi  15901  lvecindp  15907  lvecindp2  15908  lsmcv  15910  lspsolv  15912  lssacsex  15913  lspsnat  15914  lsppratlem2  15917  lsppratlem3  15918  lsppratlem4  15919  lsppratlem6  15921  lspprat  15922  islbs2  15923  islbs3  15924  lbsacsbs  15925  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  phllmod  16550  isphld  16574  islinds4  27408  lshpnelb  29796  lshpnel2N  29797  lshpdisj  29799  lshpcmp  29800  lsatcmp  29815  lsatcmp2  29816  lsatel  29817  lsatelbN  29818  lsatfixedN  29821  lsmcv2  29841  lsatcv0  29843  lsatcveq0  29844  lsat0cv  29845  lcvp  29852  lcv1  29853  lcv2  29854  lsatexch  29855  lsatnem0  29857  lsatexch1  29858  lsatcv0eq  29859  lsatcv1  29860  lsatcvatlem  29861  lsatcvat  29862  lsatcvat2  29863  lsatcvat3  29864  islshpcv  29865  l1cvpat  29866  l1cvat  29867  lfl1  29882  lkrsc  29909  lkrscss  29910  eqlkr  29911  eqlkr3  29913  lkrlsp  29914  lkrlsp3  29916  lkrshp  29917  lkrshp3  29918  lkrshpor  29919  lkrshp4  29920  lshpsmreu  29921  lshpkrlem1  29922  lshpkrlem4  29925  lshpkrlem5  29926  lshpkrlem6  29927  lshpkr  29929  lshpkrex  29930  lfl1dim  29933  lfl1dim2N  29934  lduallvec  29966  lduallkr3  29974  lkrpssN  29975  ldual1dim  29978  lkrss2N  29981  lkreqN  29982  lkrlspeqN  29983  dva0g  31839  dia1dim2  31874  dia1dimid  31875  dia2dimlem5  31880  dia2dimlem7  31882  dia2dimlem9  31884  dia2dimlem10  31885  dia2dimlem13  31888  dvhlmod  31922  diblsmopel  31983  lclkrlem2m  32331  lclkrlem2n  32332  lcfrlem1  32354  lcfrlem2  32355  lcfrlem3  32356  lcdlmod  32404  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdindp0  32531  mapdindp1  32532  mapdindp2  32533  mapdindp3  32534  mapdindp4  32535  lspindp5  32582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-lvec 15872
  Copyright terms: Public domain W3C validator