Theorem lveclmod 21013

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  Scalarcsca 17223  DivRingcdr 20638  LModclmod 20766  LVecclvec 21009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-lvec 21010

This theorem is referenced by:  lveclmodd  21014  lsslvec  21016  lvecvs0or  21018  lssvs0or  21020  lvecvscan  21021  lvecvscan2  21022  lvecinv  21023  lspsnvs  21024  lspsneleq  21025  lspsncmp  21026  lspsnne1  21027  lspsnnecom  21029  lspabs2  21030  lspabs3  21031  lspsneq  21032  ellspsn4  21034  lspdisj  21035  lspdisjb  21036  lspdisj2  21037  lspfixed  21038  lspexch  21039  lspexchn1  21040  lspindpi  21042  lvecindp  21048  lvecindp2  21049  lsmcv  21051  lspsolv  21053  lssacsex  21054  lspsnat  21055  lsppratlem2  21058  lsppratlem3  21059  lsppratlem4  21060  lsppratlem6  21062  lspprat  21063  islbs2  21064  islbs3  21065  lbsacsbs  21066  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  phllmod  21539  isphld  21563  islinds4  21744  lvecisfrlm  21752  cvsi  25030  0nellinds  33341  lindssn  33349  linds2eq  33352  exsslsb  33592  lvecdim0i  33601  lssdimle  33603  tngdim  33609  matdim  33611  lbslsat  33612  lsatdim  33613  drngdimgt0  33614  lindsunlem  33620  lindsun  33621  lbsdiflsp0  33622  dimkerim  33623  qusdimsum  33624  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  extdg1id  33661  ccfldextdgrr  33667  lindsadd  37607  lshpnelb  38977  lshpnel2N  38978  lshpdisj  38980  lshpcmp  38981  lsatcmp  38996  lsatcmp2  38997  lsatel  38998  lsatelbN  38999  lsatfixedN  39002  lsmcv2  39022  lsatcv0  39024  lsatcveq0  39025  lsat0cv  39026  lcvp  39033  lcv1  39034  lcv2  39035  lsatexch  39036  lsatnem0  39038  lsatexch1  39039  lsatcv0eq  39040  lsatcv1  39041  lsatcvatlem  39042  lsatcvat  39043  lsatcvat2  39044  lsatcvat3  39045  islshpcv  39046  l1cvpat  39047  l1cvat  39048  lfl1  39063  lkrsc  39090  lkrscss  39091  eqlkr  39092  eqlkr3  39094  lkrlsp  39095  lkrlsp3  39097  lkrshp  39098  lkrshp3  39099  lkrshpor  39100  lkrshp4  39101  lshpsmreu  39102  lshpkrlem1  39103  lshpkrlem4  39106  lshpkrlem5  39107  lshpkrlem6  39108  lshpkr  39110  lshpkrex  39111  lfl1dim  39114  lfl1dim2N  39115  lduallvec  39147  lduallkr3  39155  lkrpssN  39156  ldual1dim  39159  lkrss2N  39162  lkreqN  39163  lkrlspeqN  39164  dva0g  41021  dia1dim2  41056  dia1dimid  41057  dia2dimlem5  41062  dia2dimlem7  41064  dia2dimlem9  41066  dia2dimlem10  41067  dia2dimlem13  41070  dvhlmod  41104  diblsmopel  41165  lclkrlem2m  41513  lclkrlem2n  41514  lcfrlem1  41536  lcfrlem2  41537  lcfrlem3  41538  lcdlmod  41586  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdindp0  41713  mapdindp1  41714  mapdindp2  41715  mapdindp3  41716  mapdindp4  41717  lspindp5  41764  lvecgrp  42525  lvecring  42526  prjspersym  42595  prjsper  42596  prjspreln0  42597  prjspvs  42598  prjspeclsp  42600  0prjspn  42616  lincreslvec3  48471  isldepslvec2  48474  lindssnlvec  48475  lvecpsslmod  48496