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

Theorem lveclmod 18870
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 2606 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
21islvec 18868 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
32simplbi 474 1 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cfv 5787  Scalarcsca 15714  DivRingcdr 18513  LModclmod 18629  LVecclvec 18866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-lvec 18867
This theorem is referenced by:  lsslvec  18871  lvecvs0or  18872  lssvs0or  18874  lvecvscan  18875  lvecvscan2  18876  lvecinv  18877  lspsnvs  18878  lspsneleq  18879  lspsncmp  18880  lspsnne1  18881  lspsnnecom  18883  lspabs2  18884  lspabs3  18885  lspsneq  18886  lspsnel4  18888  lspdisj  18889  lspdisjb  18890  lspdisj2  18891  lspfixed  18892  lspexch  18893  lspexchn1  18894  lspindpi  18896  lvecindp  18902  lvecindp2  18903  lsmcv  18905  lspsolv  18907  lssacsex  18908  lspsnat  18909  lsppratlem2  18912  lsppratlem3  18913  lsppratlem4  18914  lsppratlem6  18916  lspprat  18917  islbs2  18918  islbs3  18919  lbsacsbs  18920  lbsextlem2  18923  lbsextlem3  18924  lbsextlem4  18925  phllmod  19736  isphld  19760  islinds4  19932  lvecisfrlm  19940  cvsi  22664  lshpnelb  33089  lshpnel2N  33090  lshpdisj  33092  lshpcmp  33093  lsatcmp  33108  lsatcmp2  33109  lsatel  33110  lsatelbN  33111  lsatfixedN  33114  lsmcv2  33134  lsatcv0  33136  lsatcveq0  33137  lsat0cv  33138  lcvp  33145  lcv1  33146  lcv2  33147  lsatexch  33148  lsatnem0  33150  lsatexch1  33151  lsatcv0eq  33152  lsatcv1  33153  lsatcvatlem  33154  lsatcvat  33155  lsatcvat2  33156  lsatcvat3  33157  islshpcv  33158  l1cvpat  33159  l1cvat  33160  lfl1  33175  lkrsc  33202  lkrscss  33203  eqlkr  33204  eqlkr3  33206  lkrlsp  33207  lkrlsp3  33209  lkrshp  33210  lkrshp3  33211  lkrshpor  33212  lkrshp4  33213  lshpsmreu  33214  lshpkrlem1  33215  lshpkrlem4  33218  lshpkrlem5  33219  lshpkrlem6  33220  lshpkr  33222  lshpkrex  33223  lfl1dim  33226  lfl1dim2N  33227  lduallvec  33259  lduallkr3  33267  lkrpssN  33268  ldual1dim  33271  lkrss2N  33274  lkreqN  33275  lkrlspeqN  33276  dva0g  35134  dia1dim2  35169  dia1dimid  35170  dia2dimlem5  35175  dia2dimlem7  35177  dia2dimlem9  35179  dia2dimlem10  35180  dia2dimlem13  35183  dvhlmod  35217  diblsmopel  35278  lclkrlem2m  35626  lclkrlem2n  35627  lcfrlem1  35649  lcfrlem2  35650  lcfrlem3  35651  lcdlmod  35699  baerlem3lem1  35814  baerlem5alem1  35815  baerlem5blem1  35816  baerlem3lem2  35817  baerlem5alem2  35818  baerlem5blem2  35819  baerlem5amN  35823  baerlem5bmN  35824  baerlem5abmN  35825  mapdindp0  35826  mapdindp1  35827  mapdindp2  35828  mapdindp3  35829  mapdindp4  35830  lspindp5  35877  lincreslvec3  42064  isldepslvec2  42067  lindssnlvec  42068  lvecpsslmod  42089
  Copyright terms: Public domain W3C validator