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

Theorem lveclmod 19313
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 2806 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
21islvec 19311 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
32simplbi 487 1 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  cfv 6101  Scalarcsca 16156  DivRingcdr 18951  LModclmod 19067  LVecclvec 19309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109  df-lvec 19310
This theorem is referenced by:  lsslvec  19314  lvecvs0or  19315  lssvs0or  19317  lvecvscan  19318  lvecvscan2  19319  lvecinv  19320  lspsnvs  19321  lspsneleq  19322  lspsncmp  19323  lspsnne1  19324  lspsnnecom  19326  lspabs2  19327  lspabs3  19328  lspsneq  19329  lspsnel4  19331  lspdisj  19332  lspdisjb  19333  lspdisj2  19334  lspfixed  19335  lspfixedOLD  19336  lspexch  19337  lspexchn1  19338  lspindpi  19340  lvecindp  19346  lvecindp2  19347  lsmcv  19349  lspsolv  19351  lssacsex  19352  lspsnat  19353  lsppratlem2  19357  lsppratlem3  19358  lsppratlem4  19359  lsppratlem6  19361  lspprat  19362  islbs2  19363  islbs3  19364  lbsacsbs  19365  lbsextlem2  19368  lbsextlem3  19369  lbsextlem4  19370  phllmod  20185  isphld  20209  islinds4  20384  lvecisfrlm  20392  cvsi  23142  lshpnelb  34764  lshpnel2N  34765  lshpdisj  34767  lshpcmp  34768  lsatcmp  34783  lsatcmp2  34784  lsatel  34785  lsatelbN  34786  lsatfixedN  34789  lsmcv2  34809  lsatcv0  34811  lsatcveq0  34812  lsat0cv  34813  lcvp  34820  lcv1  34821  lcv2  34822  lsatexch  34823  lsatnem0  34825  lsatexch1  34826  lsatcv0eq  34827  lsatcv1  34828  lsatcvatlem  34829  lsatcvat  34830  lsatcvat2  34831  lsatcvat3  34832  islshpcv  34833  l1cvpat  34834  l1cvat  34835  lfl1  34850  lkrsc  34877  lkrscss  34878  eqlkr  34879  eqlkr3  34881  lkrlsp  34882  lkrlsp3  34884  lkrshp  34885  lkrshp3  34886  lkrshpor  34887  lkrshp4  34888  lshpsmreu  34889  lshpkrlem1  34890  lshpkrlem4  34893  lshpkrlem5  34894  lshpkrlem6  34895  lshpkr  34897  lshpkrex  34898  lfl1dim  34901  lfl1dim2N  34902  lduallvec  34934  lduallkr3  34942  lkrpssN  34943  ldual1dim  34946  lkrss2N  34949  lkreqN  34950  lkrlspeqN  34951  dva0g  36808  dia1dim2  36843  dia1dimid  36844  dia2dimlem5  36849  dia2dimlem7  36851  dia2dimlem9  36853  dia2dimlem10  36854  dia2dimlem13  36857  dvhlmod  36891  diblsmopel  36952  lclkrlem2m  37300  lclkrlem2n  37301  lcfrlem1  37323  lcfrlem2  37324  lcfrlem3  37325  lcdlmod  37373  baerlem3lem1  37488  baerlem5alem1  37489  baerlem5blem1  37490  baerlem3lem2  37491  baerlem5alem2  37492  baerlem5blem2  37493  baerlem5amN  37497  baerlem5bmN  37498  baerlem5abmN  37499  mapdindp0  37500  mapdindp1  37501  mapdindp2  37502  mapdindp3  37503  mapdindp4  37504  lspindp5  37551  lincreslvec3  42839  isldepslvec2  42842  lindssnlvec  42843  lvecpsslmod  42864
  Copyright terms: Public domain W3C validator