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

Theorem lveclmod 17209
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 2443 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 17207 . 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 1756   ` cfv 5439  Scalarcsca 14262   DivRingcdr 16854   LModclmod 16970   LVecclvec 17205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-lvec 17206
This theorem is referenced by:  lsslvec  17210  lvecvs0or  17211  lssvs0or  17213  lvecvscan  17214  lvecvscan2  17215  lvecinv  17216  lspsnvs  17217  lspsneleq  17218  lspsncmp  17219  lspsnne1  17220  lspsnnecom  17222  lspabs2  17223  lspabs3  17224  lspsneq  17225  lspsnel4  17227  lspdisj  17228  lspdisjb  17229  lspdisj2  17230  lspfixed  17231  lspexch  17232  lspexchn1  17233  lspindpi  17235  lvecindp  17241  lvecindp2  17242  lsmcv  17244  lspsolv  17246  lssacsex  17247  lspsnat  17248  lsppratlem2  17251  lsppratlem3  17252  lsppratlem4  17253  lsppratlem6  17255  lspprat  17256  islbs2  17257  islbs3  17258  lbsacsbs  17259  lbsextlem2  17262  lbsextlem3  17263  lbsextlem4  17264  phllmod  18081  isphld  18105  islinds4  18286  lvecisfrlm  18294  lincreslvec3  31013  isldepslvec2  31016  lindssnlvec  31017  lvecpsslmod  31046  lshpnelb  32725  lshpnel2N  32726  lshpdisj  32728  lshpcmp  32729  lsatcmp  32744  lsatcmp2  32745  lsatel  32746  lsatelbN  32747  lsatfixedN  32750  lsmcv2  32770  lsatcv0  32772  lsatcveq0  32773  lsat0cv  32774  lcvp  32781  lcv1  32782  lcv2  32783  lsatexch  32784  lsatnem0  32786  lsatexch1  32787  lsatcv0eq  32788  lsatcv1  32789  lsatcvatlem  32790  lsatcvat  32791  lsatcvat2  32792  lsatcvat3  32793  islshpcv  32794  l1cvpat  32795  l1cvat  32796  lfl1  32811  lkrsc  32838  lkrscss  32839  eqlkr  32840  eqlkr3  32842  lkrlsp  32843  lkrlsp3  32845  lkrshp  32846  lkrshp3  32847  lkrshpor  32848  lkrshp4  32849  lshpsmreu  32850  lshpkrlem1  32851  lshpkrlem4  32854  lshpkrlem5  32855  lshpkrlem6  32856  lshpkr  32858  lshpkrex  32859  lfl1dim  32862  lfl1dim2N  32863  lduallvec  32895  lduallkr3  32903  lkrpssN  32904  ldual1dim  32907  lkrss2N  32910  lkreqN  32911  lkrlspeqN  32912  dva0g  34768  dia1dim2  34803  dia1dimid  34804  dia2dimlem5  34809  dia2dimlem7  34811  dia2dimlem9  34813  dia2dimlem10  34814  dia2dimlem13  34817  dvhlmod  34851  diblsmopel  34912  lclkrlem2m  35260  lclkrlem2n  35261  lcfrlem1  35283  lcfrlem2  35284  lcfrlem3  35285  lcdlmod  35333  baerlem3lem1  35448  baerlem5alem1  35449  baerlem5blem1  35450  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  baerlem5amN  35457  baerlem5bmN  35458  baerlem5abmN  35459  mapdindp0  35460  mapdindp1  35461  mapdindp2  35462  mapdindp3  35463  mapdindp4  35464  lspindp5  35511
  Copyright terms: Public domain W3C validator