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

Theorem lveclmod 16170
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 2435 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 16168 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 447 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   ` cfv 5446  Scalarcsca 13524   DivRingcdr 15827   LModclmod 15942   LVecclvec 16166
This theorem is referenced by:  lsslvec  16171  lvecvs0or  16172  lssvs0or  16174  lvecvscan  16175  lvecvscan2  16176  lvecinv  16177  lspsnvs  16178  lspsneleq  16179  lspsncmp  16180  lspsnne1  16181  lspsnnecom  16183  lspabs2  16184  lspabs3  16185  lspsneq  16186  lspsnel4  16188  lspdisj  16189  lspdisjb  16190  lspdisj2  16191  lspfixed  16192  lspexch  16193  lspexchn1  16194  lspindpi  16196  lvecindp  16202  lvecindp2  16203  lsmcv  16205  lspsolv  16207  lssacsex  16208  lspsnat  16209  lsppratlem2  16212  lsppratlem3  16213  lsppratlem4  16214  lsppratlem6  16216  lspprat  16217  islbs2  16218  islbs3  16219  lbsacsbs  16220  lbsextlem2  16223  lbsextlem3  16224  lbsextlem4  16225  phllmod  16853  isphld  16877  islinds4  27273  lshpnelb  29719  lshpnel2N  29720  lshpdisj  29722  lshpcmp  29723  lsatcmp  29738  lsatcmp2  29739  lsatel  29740  lsatelbN  29741  lsatfixedN  29744  lsmcv2  29764  lsatcv0  29766  lsatcveq0  29767  lsat0cv  29768  lcvp  29775  lcv1  29776  lcv2  29777  lsatexch  29778  lsatnem0  29780  lsatexch1  29781  lsatcv0eq  29782  lsatcv1  29783  lsatcvatlem  29784  lsatcvat  29785  lsatcvat2  29786  lsatcvat3  29787  islshpcv  29788  l1cvpat  29789  l1cvat  29790  lfl1  29805  lkrsc  29832  lkrscss  29833  eqlkr  29834  eqlkr3  29836  lkrlsp  29837  lkrlsp3  29839  lkrshp  29840  lkrshp3  29841  lkrshpor  29842  lkrshp4  29843  lshpsmreu  29844  lshpkrlem1  29845  lshpkrlem4  29848  lshpkrlem5  29849  lshpkrlem6  29850  lshpkr  29852  lshpkrex  29853  lfl1dim  29856  lfl1dim2N  29857  lduallvec  29889  lduallkr3  29897  lkrpssN  29898  ldual1dim  29901  lkrss2N  29904  lkreqN  29905  lkrlspeqN  29906  dva0g  31762  dia1dim2  31797  dia1dimid  31798  dia2dimlem5  31803  dia2dimlem7  31805  dia2dimlem9  31807  dia2dimlem10  31808  dia2dimlem13  31811  dvhlmod  31845  diblsmopel  31906  lclkrlem2m  32254  lclkrlem2n  32255  lcfrlem1  32277  lcfrlem2  32278  lcfrlem3  32279  lcdlmod  32327  baerlem3lem1  32442  baerlem5alem1  32443  baerlem5blem1  32444  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  baerlem5amN  32451  baerlem5bmN  32452  baerlem5abmN  32453  mapdindp0  32454  mapdindp1  32455  mapdindp2  32456  mapdindp3  32457  mapdindp4  32458  lspindp5  32505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-lvec 16167
  Copyright terms: Public domain W3C validator