Theorem lveclmod 21050

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

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2	1	islvec 21048	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
3	2	simplbi 497	1 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  Scalarcsca 17174  DivRingcdr 20654  LModclmod 20803  LVecclvec 21046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-lvec 21047

This theorem is referenced by:  lveclmodd  21051  lsslvec  21053  lvecvs0or  21055  lssvs0or  21057  lvecvscan  21058  lvecvscan2  21059  lvecinv  21060  lspsnvs  21061  lspsneleq  21062  lspsncmp  21063  lspsnne1  21064  lspsnnecom  21066  lspabs2  21067  lspabs3  21068  lspsneq  21069  ellspsn4  21071  lspdisj  21072  lspdisjb  21073  lspdisj2  21074  lspfixed  21075  lspexch  21076  lspexchn1  21077  lspindpi  21079  lvecindp  21085  lvecindp2  21086  lsmcv  21088  lspsolv  21090  lssacsex  21091  lspsnat  21092  lsppratlem2  21095  lsppratlem3  21096  lsppratlem4  21097  lsppratlem6  21099  lspprat  21100  islbs2  21101  islbs3  21102  lbsacsbs  21103  lbsextlem2  21106  lbsextlem3  21107  lbsextlem4  21108  phllmod  21577  isphld  21601  islinds4  21782  lvecisfrlm  21790  cvsi  25067  0nellinds  33346  lindssn  33354  linds2eq  33357  exsslsb  33620  lvecdim0i  33629  lssdimle  33631  tngdim  33637  matdim  33639  lbslsat  33640  lsatdim  33641  drngdimgt0  33642  lindsunlem  33648  lindsun  33649  lbsdiflsp0  33650  dimkerim  33651  qusdimsum  33652  fedgmullem1  33653  fedgmullem2  33654  fedgmul  33655  extdg1id  33690  ccfldextdgrr  33696  lindsadd  37663  lshpnelb  39093  lshpnel2N  39094  lshpdisj  39096  lshpcmp  39097  lsatcmp  39112  lsatcmp2  39113  lsatel  39114  lsatelbN  39115  lsatfixedN  39118  lsmcv2  39138  lsatcv0  39140  lsatcveq0  39141  lsat0cv  39142  lcvp  39149  lcv1  39150  lcv2  39151  lsatexch  39152  lsatnem0  39154  lsatexch1  39155  lsatcv0eq  39156  lsatcv1  39157  lsatcvatlem  39158  lsatcvat  39159  lsatcvat2  39160  lsatcvat3  39161  islshpcv  39162  l1cvpat  39163  l1cvat  39164  lfl1  39179  lkrsc  39206  lkrscss  39207  eqlkr  39208  eqlkr3  39210  lkrlsp  39211  lkrlsp3  39213  lkrshp  39214  lkrshp3  39215  lkrshpor  39216  lkrshp4  39217  lshpsmreu  39218  lshpkrlem1  39219  lshpkrlem4  39222  lshpkrlem5  39223  lshpkrlem6  39224  lshpkr  39226  lshpkrex  39227  lfl1dim  39230  lfl1dim2N  39231  lduallvec  39263  lduallkr3  39271  lkrpssN  39272  ldual1dim  39275  lkrss2N  39278  lkreqN  39279  lkrlspeqN  39280  dva0g  41136  dia1dim2  41171  dia1dimid  41172  dia2dimlem5  41177  dia2dimlem7  41179  dia2dimlem9  41181  dia2dimlem10  41182  dia2dimlem13  41185  dvhlmod  41219  diblsmopel  41280  lclkrlem2m  41628  lclkrlem2n  41629  lcfrlem1  41651  lcfrlem2  41652  lcfrlem3  41653  lcdlmod  41701  baerlem3lem1  41816  baerlem5alem1  41817  baerlem5blem1  41818  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  baerlem5amN  41825  baerlem5bmN  41826  baerlem5abmN  41827  mapdindp0  41828  mapdindp1  41829  mapdindp2  41830  mapdindp3  41831  mapdindp4  41832  lspindp5  41879  lvecgrp  42645  lvecring  42646  prjspersym  42715  prjsper  42716  prjspreln0  42717  prjspvs  42718  prjspeclsp  42720  0prjspn  42736  lincreslvec3  48597  isldepslvec2  48600  lindssnlvec  48601  lvecpsslmod  48622