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

Theorem lveclmod 19308
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 2760 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
21islvec 19306 . 2 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
32simplbi 478 1 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cfv 6049  Scalarcsca 16146  DivRingcdr 18949  LModclmod 19065  LVecclvec 19304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-lvec 19305
This theorem is referenced by:  lsslvec  19309  lvecvs0or  19310  lssvs0or  19312  lvecvscan  19313  lvecvscan2  19314  lvecinv  19315  lspsnvs  19316  lspsneleq  19317  lspsncmp  19318  lspsnne1  19319  lspsnnecom  19321  lspabs2  19322  lspabs3  19323  lspsneq  19324  lspsnel4  19326  lspdisj  19327  lspdisjb  19328  lspdisj2  19329  lspfixed  19330  lspexch  19331  lspexchn1  19332  lspindpi  19334  lvecindp  19340  lvecindp2  19341  lsmcv  19343  lspsolv  19345  lssacsex  19346  lspsnat  19347  lsppratlem2  19350  lsppratlem3  19351  lsppratlem4  19352  lsppratlem6  19354  lspprat  19355  islbs2  19356  islbs3  19357  lbsacsbs  19358  lbsextlem2  19361  lbsextlem3  19362  lbsextlem4  19363  phllmod  20177  isphld  20201  islinds4  20376  lvecisfrlm  20384  cvsi  23130  lshpnelb  34774  lshpnel2N  34775  lshpdisj  34777  lshpcmp  34778  lsatcmp  34793  lsatcmp2  34794  lsatel  34795  lsatelbN  34796  lsatfixedN  34799  lsmcv2  34819  lsatcv0  34821  lsatcveq0  34822  lsat0cv  34823  lcvp  34830  lcv1  34831  lcv2  34832  lsatexch  34833  lsatnem0  34835  lsatexch1  34836  lsatcv0eq  34837  lsatcv1  34838  lsatcvatlem  34839  lsatcvat  34840  lsatcvat2  34841  lsatcvat3  34842  islshpcv  34843  l1cvpat  34844  l1cvat  34845  lfl1  34860  lkrsc  34887  lkrscss  34888  eqlkr  34889  eqlkr3  34891  lkrlsp  34892  lkrlsp3  34894  lkrshp  34895  lkrshp3  34896  lkrshpor  34897  lkrshp4  34898  lshpsmreu  34899  lshpkrlem1  34900  lshpkrlem4  34903  lshpkrlem5  34904  lshpkrlem6  34905  lshpkr  34907  lshpkrex  34908  lfl1dim  34911  lfl1dim2N  34912  lduallvec  34944  lduallkr3  34952  lkrpssN  34953  ldual1dim  34956  lkrss2N  34959  lkreqN  34960  lkrlspeqN  34961  dva0g  36818  dia1dim2  36853  dia1dimid  36854  dia2dimlem5  36859  dia2dimlem7  36861  dia2dimlem9  36863  dia2dimlem10  36864  dia2dimlem13  36867  dvhlmod  36901  diblsmopel  36962  lclkrlem2m  37310  lclkrlem2n  37311  lcfrlem1  37333  lcfrlem2  37334  lcfrlem3  37335  lcdlmod  37383  baerlem3lem1  37498  baerlem5alem1  37499  baerlem5blem1  37500  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  baerlem5amN  37507  baerlem5bmN  37508  baerlem5abmN  37509  mapdindp0  37510  mapdindp1  37511  mapdindp2  37512  mapdindp3  37513  mapdindp4  37514  lspindp5  37561  lincreslvec3  42781  isldepslvec2  42784  lindssnlvec  42785  lvecpsslmod  42806
  Copyright terms: Public domain W3C validator