Theorem lveclmod 20283

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  Scalarcsca 16891  DivRingcdr 19906  LModclmod 20038  LVecclvec 20279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-lvec 20280

This theorem is referenced by:  lsslvec  20284  lvecvs0or  20285  lssvs0or  20287  lvecvscan  20288  lvecvscan2  20289  lvecinv  20290  lspsnvs  20291  lspsneleq  20292  lspsncmp  20293  lspsnne1  20294  lspsnnecom  20296  lspabs2  20297  lspabs3  20298  lspsneq  20299  lspsnel4  20301  lspdisj  20302  lspdisjb  20303  lspdisj2  20304  lspfixed  20305  lspexch  20306  lspexchn1  20307  lspindpi  20309  lvecindp  20315  lvecindp2  20316  lsmcv  20318  lspsolv  20320  lssacsex  20321  lspsnat  20322  lsppratlem2  20325  lsppratlem3  20326  lsppratlem4  20327  lsppratlem6  20329  lspprat  20330  islbs2  20331  islbs3  20332  lbsacsbs  20333  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  phllmod  20747  isphld  20771  islinds4  20952  lvecisfrlm  20960  cvsi  24199  0nellinds  31468  lindssn  31475  linds2eq  31477  lvecdim0i  31591  lssdimle  31593  tngdim  31598  matdim  31600  lbslsat  31601  lsatdim  31602  drngdimgt0  31603  lindsunlem  31607  lindsun  31608  lbsdiflsp0  31609  dimkerim  31610  qusdimsum  31611  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  extdg1id  31640  ccfldextdgrr  31644  lindsadd  35697  lshpnelb  36925  lshpnel2N  36926  lshpdisj  36928  lshpcmp  36929  lsatcmp  36944  lsatcmp2  36945  lsatel  36946  lsatelbN  36947  lsatfixedN  36950  lsmcv2  36970  lsatcv0  36972  lsatcveq0  36973  lsat0cv  36974  lcvp  36981  lcv1  36982  lcv2  36983  lsatexch  36984  lsatnem0  36986  lsatexch1  36987  lsatcv0eq  36988  lsatcv1  36989  lsatcvatlem  36990  lsatcvat  36991  lsatcvat2  36992  lsatcvat3  36993  islshpcv  36994  l1cvpat  36995  l1cvat  36996  lfl1  37011  lkrsc  37038  lkrscss  37039  eqlkr  37040  eqlkr3  37042  lkrlsp  37043  lkrlsp3  37045  lkrshp  37046  lkrshp3  37047  lkrshpor  37048  lkrshp4  37049  lshpsmreu  37050  lshpkrlem1  37051  lshpkrlem4  37054  lshpkrlem5  37055  lshpkrlem6  37056  lshpkr  37058  lshpkrex  37059  lfl1dim  37062  lfl1dim2N  37063  lduallvec  37095  lduallkr3  37103  lkrpssN  37104  ldual1dim  37107  lkrss2N  37110  lkreqN  37111  lkrlspeqN  37112  dva0g  38968  dia1dim2  39003  dia1dimid  39004  dia2dimlem5  39009  dia2dimlem7  39011  dia2dimlem9  39013  dia2dimlem10  39014  dia2dimlem13  39017  dvhlmod  39051  diblsmopel  39112  lclkrlem2m  39460  lclkrlem2n  39461  lcfrlem1  39483  lcfrlem2  39484  lcfrlem3  39485  lcdlmod  39533  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdindp0  39660  mapdindp1  39661  mapdindp2  39662  mapdindp3  39663  mapdindp4  39664  lspindp5  39711  lvecgrp  40182  lveclmodd  40183  lvecring  40185  prjspersym  40367  prjsper  40368  prjspreln0  40369  prjspvs  40370  prjspeclsp  40372  0prjspn  40386  lincreslvec3  45711  isldepslvec2  45714  lindssnlvec  45715  lvecpsslmod  45736