Theorem lveclmod 21028

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6486  Scalarcsca 17182  DivRingcdr 20632  LModclmod 20781  LVecclvec 21024

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-lvec 21025

This theorem is referenced by:  lveclmodd  21029  lsslvec  21031  lvecvs0or  21033  lssvs0or  21035  lvecvscan  21036  lvecvscan2  21037  lvecinv  21038  lspsnvs  21039  lspsneleq  21040  lspsncmp  21041  lspsnne1  21042  lspsnnecom  21044  lspabs2  21045  lspabs3  21046  lspsneq  21047  ellspsn4  21049  lspdisj  21050  lspdisjb  21051  lspdisj2  21052  lspfixed  21053  lspexch  21054  lspexchn1  21055  lspindpi  21057  lvecindp  21063  lvecindp2  21064  lsmcv  21066  lspsolv  21068  lssacsex  21069  lspsnat  21070  lsppratlem2  21073  lsppratlem3  21074  lsppratlem4  21075  lsppratlem6  21077  lspprat  21078  islbs2  21079  islbs3  21080  lbsacsbs  21081  lbsextlem2  21084  lbsextlem3  21085  lbsextlem4  21086  phllmod  21555  isphld  21579  islinds4  21760  lvecisfrlm  21768  cvsi  25046  0nellinds  33317  lindssn  33325  linds2eq  33328  exsslsb  33568  lvecdim0i  33577  lssdimle  33579  tngdim  33585  matdim  33587  lbslsat  33588  lsatdim  33589  drngdimgt0  33590  lindsunlem  33596  lindsun  33597  lbsdiflsp0  33598  dimkerim  33599  qusdimsum  33600  fedgmullem1  33601  fedgmullem2  33602  fedgmul  33603  extdg1id  33637  ccfldextdgrr  33643  lindsadd  37592  lshpnelb  38962  lshpnel2N  38963  lshpdisj  38965  lshpcmp  38966  lsatcmp  38981  lsatcmp2  38982  lsatel  38983  lsatelbN  38984  lsatfixedN  38987  lsmcv2  39007  lsatcv0  39009  lsatcveq0  39010  lsat0cv  39011  lcvp  39018  lcv1  39019  lcv2  39020  lsatexch  39021  lsatnem0  39023  lsatexch1  39024  lsatcv0eq  39025  lsatcv1  39026  lsatcvatlem  39027  lsatcvat  39028  lsatcvat2  39029  lsatcvat3  39030  islshpcv  39031  l1cvpat  39032  l1cvat  39033  lfl1  39048  lkrsc  39075  lkrscss  39076  eqlkr  39077  eqlkr3  39079  lkrlsp  39080  lkrlsp3  39082  lkrshp  39083  lkrshp3  39084  lkrshpor  39085  lkrshp4  39086  lshpsmreu  39087  lshpkrlem1  39088  lshpkrlem4  39091  lshpkrlem5  39092  lshpkrlem6  39093  lshpkr  39095  lshpkrex  39096  lfl1dim  39099  lfl1dim2N  39100  lduallvec  39132  lduallkr3  39140  lkrpssN  39141  ldual1dim  39144  lkrss2N  39147  lkreqN  39148  lkrlspeqN  39149  dva0g  41006  dia1dim2  41041  dia1dimid  41042  dia2dimlem5  41047  dia2dimlem7  41049  dia2dimlem9  41051  dia2dimlem10  41052  dia2dimlem13  41055  dvhlmod  41089  diblsmopel  41150  lclkrlem2m  41498  lclkrlem2n  41499  lcfrlem1  41521  lcfrlem2  41522  lcfrlem3  41523  lcdlmod  41571  baerlem3lem1  41686  baerlem5alem1  41687  baerlem5blem1  41688  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  mapdindp0  41698  mapdindp1  41699  mapdindp2  41700  mapdindp3  41701  mapdindp4  41702  lspindp5  41749  lvecgrp  42510  lvecring  42511  prjspersym  42580  prjsper  42581  prjspreln0  42582  prjspvs  42583  prjspeclsp  42585  0prjspn  42601  lincreslvec3  48455  isldepslvec2  48458  lindssnlvec  48459  lvecpsslmod  48480