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

Theorem lveclmod 18074
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 2404 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 18072 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 460 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1844   ` cfv 5571  Scalarcsca 14914   DivRingcdr 17718   LModclmod 17834   LVecclvec 18070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-iota 5535  df-fv 5579  df-lvec 18071
This theorem is referenced by:  lsslvec  18075  lvecvs0or  18076  lssvs0or  18078  lvecvscan  18079  lvecvscan2  18080  lvecinv  18081  lspsnvs  18082  lspsneleq  18083  lspsncmp  18084  lspsnne1  18085  lspsnnecom  18087  lspabs2  18088  lspabs3  18089  lspsneq  18090  lspsnel4  18092  lspdisj  18093  lspdisjb  18094  lspdisj2  18095  lspfixed  18096  lspexch  18097  lspexchn1  18098  lspindpi  18100  lvecindp  18106  lvecindp2  18107  lsmcv  18109  lspsolv  18111  lssacsex  18112  lspsnat  18113  lsppratlem2  18116  lsppratlem3  18117  lsppratlem4  18118  lsppratlem6  18120  lspprat  18121  islbs2  18122  islbs3  18123  lbsacsbs  18124  lbsextlem2  18127  lbsextlem3  18128  lbsextlem4  18129  phllmod  18965  isphld  18989  islinds4  19164  lvecisfrlm  19172  lshpnelb  32015  lshpnel2N  32016  lshpdisj  32018  lshpcmp  32019  lsatcmp  32034  lsatcmp2  32035  lsatel  32036  lsatelbN  32037  lsatfixedN  32040  lsmcv2  32060  lsatcv0  32062  lsatcveq0  32063  lsat0cv  32064  lcvp  32071  lcv1  32072  lcv2  32073  lsatexch  32074  lsatnem0  32076  lsatexch1  32077  lsatcv0eq  32078  lsatcv1  32079  lsatcvatlem  32080  lsatcvat  32081  lsatcvat2  32082  lsatcvat3  32083  islshpcv  32084  l1cvpat  32085  l1cvat  32086  lfl1  32101  lkrsc  32128  lkrscss  32129  eqlkr  32130  eqlkr3  32132  lkrlsp  32133  lkrlsp3  32135  lkrshp  32136  lkrshp3  32137  lkrshpor  32138  lkrshp4  32139  lshpsmreu  32140  lshpkrlem1  32141  lshpkrlem4  32144  lshpkrlem5  32145  lshpkrlem6  32146  lshpkr  32148  lshpkrex  32149  lfl1dim  32152  lfl1dim2N  32153  lduallvec  32185  lduallkr3  32193  lkrpssN  32194  ldual1dim  32197  lkrss2N  32200  lkreqN  32201  lkrlspeqN  32202  dva0g  34060  dia1dim2  34095  dia1dimid  34096  dia2dimlem5  34101  dia2dimlem7  34103  dia2dimlem9  34105  dia2dimlem10  34106  dia2dimlem13  34109  dvhlmod  34143  diblsmopel  34204  lclkrlem2m  34552  lclkrlem2n  34553  lcfrlem1  34575  lcfrlem2  34576  lcfrlem3  34577  lcdlmod  34625  baerlem3lem1  34740  baerlem5alem1  34741  baerlem5blem1  34742  baerlem3lem2  34743  baerlem5alem2  34744  baerlem5blem2  34745  baerlem5amN  34749  baerlem5bmN  34750  baerlem5abmN  34751  mapdindp0  34752  mapdindp1  34753  mapdindp2  34754  mapdindp3  34755  mapdindp4  34756  lspindp5  34803  lincreslvec3  38607  isldepslvec2  38610  lindssnlvec  38611  lvecpsslmod  38632
  Copyright terms: Public domain W3C validator