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

Theorem lveclmod 16183
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 2438 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 16181 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 448 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   ` cfv 5457  Scalarcsca 13537   DivRingcdr 15840   LModclmod 15955   LVecclvec 16179
This theorem is referenced by:  lsslvec  16184  lvecvs0or  16185  lssvs0or  16187  lvecvscan  16188  lvecvscan2  16189  lvecinv  16190  lspsnvs  16191  lspsneleq  16192  lspsncmp  16193  lspsnne1  16194  lspsnnecom  16196  lspabs2  16197  lspabs3  16198  lspsneq  16199  lspsnel4  16201  lspdisj  16202  lspdisjb  16203  lspdisj2  16204  lspfixed  16205  lspexch  16206  lspexchn1  16207  lspindpi  16209  lvecindp  16215  lvecindp2  16216  lsmcv  16218  lspsolv  16220  lssacsex  16221  lspsnat  16222  lsppratlem2  16225  lsppratlem3  16226  lsppratlem4  16227  lsppratlem6  16229  lspprat  16230  islbs2  16231  islbs3  16232  lbsacsbs  16233  lbsextlem2  16236  lbsextlem3  16237  lbsextlem4  16238  phllmod  16866  isphld  16890  islinds4  27296  lshpnelb  29856  lshpnel2N  29857  lshpdisj  29859  lshpcmp  29860  lsatcmp  29875  lsatcmp2  29876  lsatel  29877  lsatelbN  29878  lsatfixedN  29881  lsmcv2  29901  lsatcv0  29903  lsatcveq0  29904  lsat0cv  29905  lcvp  29912  lcv1  29913  lcv2  29914  lsatexch  29915  lsatnem0  29917  lsatexch1  29918  lsatcv0eq  29919  lsatcv1  29920  lsatcvatlem  29921  lsatcvat  29922  lsatcvat2  29923  lsatcvat3  29924  islshpcv  29925  l1cvpat  29926  l1cvat  29927  lfl1  29942  lkrsc  29969  lkrscss  29970  eqlkr  29971  eqlkr3  29973  lkrlsp  29974  lkrlsp3  29976  lkrshp  29977  lkrshp3  29978  lkrshpor  29979  lkrshp4  29980  lshpsmreu  29981  lshpkrlem1  29982  lshpkrlem4  29985  lshpkrlem5  29986  lshpkrlem6  29987  lshpkr  29989  lshpkrex  29990  lfl1dim  29993  lfl1dim2N  29994  lduallvec  30026  lduallkr3  30034  lkrpssN  30035  ldual1dim  30038  lkrss2N  30041  lkreqN  30042  lkrlspeqN  30043  dva0g  31899  dia1dim2  31934  dia1dimid  31935  dia2dimlem5  31940  dia2dimlem7  31942  dia2dimlem9  31944  dia2dimlem10  31945  dia2dimlem13  31948  dvhlmod  31982  diblsmopel  32043  lclkrlem2m  32391  lclkrlem2n  32392  lcfrlem1  32414  lcfrlem2  32415  lcfrlem3  32416  lcdlmod  32464  baerlem3lem1  32579  baerlem5alem1  32580  baerlem5blem1  32581  baerlem3lem2  32582  baerlem5alem2  32583  baerlem5blem2  32584  baerlem5amN  32588  baerlem5bmN  32589  baerlem5abmN  32590  mapdindp0  32591  mapdindp1  32592  mapdindp2  32593  mapdindp3  32594  mapdindp4  32595  lspindp5  32642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-lvec 16180
  Copyright terms: Public domain W3C validator