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

Theorem lveclmod 19087
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 2620 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
21islvec 19085 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
32simplbi 476 1 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cfv 5876  Scalarcsca 15925  DivRingcdr 18728  LModclmod 18844  LVecclvec 19083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-lvec 19084
This theorem is referenced by:  lsslvec  19088  lvecvs0or  19089  lssvs0or  19091  lvecvscan  19092  lvecvscan2  19093  lvecinv  19094  lspsnvs  19095  lspsneleq  19096  lspsncmp  19097  lspsnne1  19098  lspsnnecom  19100  lspabs2  19101  lspabs3  19102  lspsneq  19103  lspsnel4  19105  lspdisj  19106  lspdisjb  19107  lspdisj2  19108  lspfixed  19109  lspexch  19110  lspexchn1  19111  lspindpi  19113  lvecindp  19119  lvecindp2  19120  lsmcv  19122  lspsolv  19124  lssacsex  19125  lspsnat  19126  lsppratlem2  19129  lsppratlem3  19130  lsppratlem4  19131  lsppratlem6  19133  lspprat  19134  islbs2  19135  islbs3  19136  lbsacsbs  19137  lbsextlem2  19140  lbsextlem3  19141  lbsextlem4  19142  phllmod  19956  isphld  19980  islinds4  20155  lvecisfrlm  20163  cvsi  22911  lshpnelb  34090  lshpnel2N  34091  lshpdisj  34093  lshpcmp  34094  lsatcmp  34109  lsatcmp2  34110  lsatel  34111  lsatelbN  34112  lsatfixedN  34115  lsmcv2  34135  lsatcv0  34137  lsatcveq0  34138  lsat0cv  34139  lcvp  34146  lcv1  34147  lcv2  34148  lsatexch  34149  lsatnem0  34151  lsatexch1  34152  lsatcv0eq  34153  lsatcv1  34154  lsatcvatlem  34155  lsatcvat  34156  lsatcvat2  34157  lsatcvat3  34158  islshpcv  34159  l1cvpat  34160  l1cvat  34161  lfl1  34176  lkrsc  34203  lkrscss  34204  eqlkr  34205  eqlkr3  34207  lkrlsp  34208  lkrlsp3  34210  lkrshp  34211  lkrshp3  34212  lkrshpor  34213  lkrshp4  34214  lshpsmreu  34215  lshpkrlem1  34216  lshpkrlem4  34219  lshpkrlem5  34220  lshpkrlem6  34221  lshpkr  34223  lshpkrex  34224  lfl1dim  34227  lfl1dim2N  34228  lduallvec  34260  lduallkr3  34268  lkrpssN  34269  ldual1dim  34272  lkrss2N  34275  lkreqN  34276  lkrlspeqN  34277  dva0g  36135  dia1dim2  36170  dia1dimid  36171  dia2dimlem5  36176  dia2dimlem7  36178  dia2dimlem9  36180  dia2dimlem10  36181  dia2dimlem13  36184  dvhlmod  36218  diblsmopel  36279  lclkrlem2m  36627  lclkrlem2n  36628  lcfrlem1  36650  lcfrlem2  36651  lcfrlem3  36652  lcdlmod  36700  baerlem3lem1  36815  baerlem5alem1  36816  baerlem5blem1  36817  baerlem3lem2  36818  baerlem5alem2  36819  baerlem5blem2  36820  baerlem5amN  36824  baerlem5bmN  36825  baerlem5abmN  36826  mapdindp0  36827  mapdindp1  36828  mapdindp2  36829  mapdindp3  36830  mapdindp4  36831  lspindp5  36878  lincreslvec3  42036  isldepslvec2  42039  lindssnlvec  42040  lvecpsslmod  42061
  Copyright terms: Public domain W3C validator