Theorem lveclmod 21033

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 2730	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2	1	islvec 21031	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
3	2	simplbi 497	1 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2110  ‘cfv 6477  Scalarcsca 17156  DivRingcdr 20637  LModclmod 20786  LVecclvec 21029

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 2112  ax-9 2120  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-lvec 21030

This theorem is referenced by:  lveclmodd  21034  lsslvec  21036  lvecvs0or  21038  lssvs0or  21040  lvecvscan  21041  lvecvscan2  21042  lvecinv  21043  lspsnvs  21044  lspsneleq  21045  lspsncmp  21046  lspsnne1  21047  lspsnnecom  21049  lspabs2  21050  lspabs3  21051  lspsneq  21052  ellspsn4  21054  lspdisj  21055  lspdisjb  21056  lspdisj2  21057  lspfixed  21058  lspexch  21059  lspexchn1  21060  lspindpi  21062  lvecindp  21068  lvecindp2  21069  lsmcv  21071  lspsolv  21073  lssacsex  21074  lspsnat  21075  lsppratlem2  21078  lsppratlem3  21079  lsppratlem4  21080  lsppratlem6  21082  lspprat  21083  islbs2  21084  islbs3  21085  lbsacsbs  21086  lbsextlem2  21089  lbsextlem3  21090  lbsextlem4  21091  phllmod  21560  isphld  21584  islinds4  21765  lvecisfrlm  21773  cvsi  25050  0nellinds  33325  lindssn  33333  linds2eq  33336  exsslsb  33599  lvecdim0i  33608  lssdimle  33610  tngdim  33616  matdim  33618  lbslsat  33619  lsatdim  33620  drngdimgt0  33621  lindsunlem  33627  lindsun  33628  lbsdiflsp0  33629  dimkerim  33630  qusdimsum  33631  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdg1id  33669  ccfldextdgrr  33675  lindsadd  37632  lshpnelb  39002  lshpnel2N  39003  lshpdisj  39005  lshpcmp  39006  lsatcmp  39021  lsatcmp2  39022  lsatel  39023  lsatelbN  39024  lsatfixedN  39027  lsmcv2  39047  lsatcv0  39049  lsatcveq0  39050  lsat0cv  39051  lcvp  39058  lcv1  39059  lcv2  39060  lsatexch  39061  lsatnem0  39063  lsatexch1  39064  lsatcv0eq  39065  lsatcv1  39066  lsatcvatlem  39067  lsatcvat  39068  lsatcvat2  39069  lsatcvat3  39070  islshpcv  39071  l1cvpat  39072  l1cvat  39073  lfl1  39088  lkrsc  39115  lkrscss  39116  eqlkr  39117  eqlkr3  39119  lkrlsp  39120  lkrlsp3  39122  lkrshp  39123  lkrshp3  39124  lkrshpor  39125  lkrshp4  39126  lshpsmreu  39127  lshpkrlem1  39128  lshpkrlem4  39131  lshpkrlem5  39132  lshpkrlem6  39133  lshpkr  39135  lshpkrex  39136  lfl1dim  39139  lfl1dim2N  39140  lduallvec  39172  lduallkr3  39180  lkrpssN  39181  ldual1dim  39184  lkrss2N  39187  lkreqN  39188  lkrlspeqN  39189  dva0g  41045  dia1dim2  41080  dia1dimid  41081  dia2dimlem5  41086  dia2dimlem7  41088  dia2dimlem9  41090  dia2dimlem10  41091  dia2dimlem13  41094  dvhlmod  41128  diblsmopel  41189  lclkrlem2m  41537  lclkrlem2n  41538  lcfrlem1  41560  lcfrlem2  41561  lcfrlem3  41562  lcdlmod  41610  baerlem3lem1  41725  baerlem5alem1  41726  baerlem5blem1  41727  baerlem3lem2  41728  baerlem5alem2  41729  baerlem5blem2  41730  baerlem5amN  41734  baerlem5bmN  41735  baerlem5abmN  41736  mapdindp0  41737  mapdindp1  41738  mapdindp2  41739  mapdindp3  41740  mapdindp4  41741  lspindp5  41788  lvecgrp  42549  lvecring  42550  prjspersym  42619  prjsper  42620  prjspreln0  42621  prjspvs  42622  prjspeclsp  42624  0prjspn  42640  lincreslvec3  48493  isldepslvec2  48496  lindssnlvec  48497  lvecpsslmod  48518