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

Theorem lveclmod 19853
Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)
Assertion
Ref Expression
lveclmod (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Proof of Theorem lveclmod
StepHypRef Expression
1 eqid 2821 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
21islvec 19851 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
32simplbi 501 1 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cfv 6328  Scalarcsca 16546  DivRingcdr 19477  LModclmod 19609  LVecclvec 19849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-lvec 19850
This theorem is referenced by:  lsslvec  19854  lvecvs0or  19855  lssvs0or  19857  lvecvscan  19858  lvecvscan2  19859  lvecinv  19860  lspsnvs  19861  lspsneleq  19862  lspsncmp  19863  lspsnne1  19864  lspsnnecom  19866  lspabs2  19867  lspabs3  19868  lspsneq  19869  lspsnel4  19871  lspdisj  19872  lspdisjb  19873  lspdisj2  19874  lspfixed  19875  lspexch  19876  lspexchn1  19877  lspindpi  19879  lvecindp  19885  lvecindp2  19886  lsmcv  19888  lspsolv  19890  lssacsex  19891  lspsnat  19892  lsppratlem2  19895  lsppratlem3  19896  lsppratlem4  19897  lsppratlem6  19899  lspprat  19900  islbs2  19901  islbs3  19902  lbsacsbs  19903  lbsextlem2  19906  lbsextlem3  19907  lbsextlem4  19908  phllmod  20749  isphld  20773  islinds4  20954  lvecisfrlm  20962  cvsi  23713  0nellinds  30942  lindssn  30947  linds2eq  30949  lvecdim0i  31014  lssdimle  31016  tngdim  31021  matdim  31023  lbslsat  31024  lsatdim  31025  drngdimgt0  31026  lindsunlem  31030  lindsun  31031  lbsdiflsp0  31032  dimkerim  31033  qusdimsum  31034  fedgmullem1  31035  fedgmullem2  31036  fedgmul  31037  extdg1id  31063  ccfldextdgrr  31067  lindsadd  34928  lshpnelb  36158  lshpnel2N  36159  lshpdisj  36161  lshpcmp  36162  lsatcmp  36177  lsatcmp2  36178  lsatel  36179  lsatelbN  36180  lsatfixedN  36183  lsmcv2  36203  lsatcv0  36205  lsatcveq0  36206  lsat0cv  36207  lcvp  36214  lcv1  36215  lcv2  36216  lsatexch  36217  lsatnem0  36219  lsatexch1  36220  lsatcv0eq  36221  lsatcv1  36222  lsatcvatlem  36223  lsatcvat  36224  lsatcvat2  36225  lsatcvat3  36226  islshpcv  36227  l1cvpat  36228  l1cvat  36229  lfl1  36244  lkrsc  36271  lkrscss  36272  eqlkr  36273  eqlkr3  36275  lkrlsp  36276  lkrlsp3  36278  lkrshp  36279  lkrshp3  36280  lkrshpor  36281  lkrshp4  36282  lshpsmreu  36283  lshpkrlem1  36284  lshpkrlem4  36287  lshpkrlem5  36288  lshpkrlem6  36289  lshpkr  36291  lshpkrex  36292  lfl1dim  36295  lfl1dim2N  36296  lduallvec  36328  lduallkr3  36336  lkrpssN  36337  ldual1dim  36340  lkrss2N  36343  lkreqN  36344  lkrlspeqN  36345  dva0g  38201  dia1dim2  38236  dia1dimid  38237  dia2dimlem5  38242  dia2dimlem7  38244  dia2dimlem9  38246  dia2dimlem10  38247  dia2dimlem13  38250  dvhlmod  38284  diblsmopel  38345  lclkrlem2m  38693  lclkrlem2n  38694  lcfrlem1  38716  lcfrlem2  38717  lcfrlem3  38718  lcdlmod  38766  baerlem3lem1  38881  baerlem5alem1  38882  baerlem5blem1  38883  baerlem3lem2  38884  baerlem5alem2  38885  baerlem5blem2  38886  baerlem5amN  38890  baerlem5bmN  38891  baerlem5abmN  38892  mapdindp0  38893  mapdindp1  38894  mapdindp2  38895  mapdindp3  38896  mapdindp4  38897  lspindp5  38944  lvecgrp  39266  lveclmodd  39267  lvecring  39269  prjspersym  39396  prjsper  39397  prjspreln0  39398  prjspvs  39399  prjspeclsp  39401  0prjspn  39409  lincreslvec3  44682  isldepslvec2  44685  lindssnlvec  44686  lvecpsslmod  44707
  Copyright terms: Public domain W3C validator