Theorem lveclmod 20709

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6540  Scalarcsca 17196  DivRingcdr 20307  LModclmod 20463  LVecclvec 20705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-lvec 20706

This theorem is referenced by:  lveclmodd  20710  lsslvec  20711  lvecvs0or  20713  lssvs0or  20715  lvecvscan  20716  lvecvscan2  20717  lvecinv  20718  lspsnvs  20719  lspsneleq  20720  lspsncmp  20721  lspsnne1  20722  lspsnnecom  20724  lspabs2  20725  lspabs3  20726  lspsneq  20727  lspsnel4  20729  lspdisj  20730  lspdisjb  20731  lspdisj2  20732  lspfixed  20733  lspexch  20734  lspexchn1  20735  lspindpi  20737  lvecindp  20743  lvecindp2  20744  lsmcv  20746  lspsolv  20748  lssacsex  20749  lspsnat  20750  lsppratlem2  20753  lsppratlem3  20754  lsppratlem4  20755  lsppratlem6  20757  lspprat  20758  islbs2  20759  islbs3  20760  lbsacsbs  20761  lbsextlem2  20764  lbsextlem3  20765  lbsextlem4  20766  phllmod  21174  isphld  21198  islinds4  21381  lvecisfrlm  21389  cvsi  24637  0nellinds  32471  lindssn  32482  linds2eq  32485  lvecdim0i  32678  lssdimle  32680  tngdim  32686  matdim  32688  lbslsat  32689  lsatdim  32690  drngdimgt0  32691  lindsunlem  32697  lindsun  32698  lbsdiflsp0  32699  dimkerim  32700  qusdimsum  32701  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  extdg1id  32730  ccfldextdgrr  32734  lindsadd  36469  lshpnelb  37842  lshpnel2N  37843  lshpdisj  37845  lshpcmp  37846  lsatcmp  37861  lsatcmp2  37862  lsatel  37863  lsatelbN  37864  lsatfixedN  37867  lsmcv2  37887  lsatcv0  37889  lsatcveq0  37890  lsat0cv  37891  lcvp  37898  lcv1  37899  lcv2  37900  lsatexch  37901  lsatnem0  37903  lsatexch1  37904  lsatcv0eq  37905  lsatcv1  37906  lsatcvatlem  37907  lsatcvat  37908  lsatcvat2  37909  lsatcvat3  37910  islshpcv  37911  l1cvpat  37912  l1cvat  37913  lfl1  37928  lkrsc  37955  lkrscss  37956  eqlkr  37957  eqlkr3  37959  lkrlsp  37960  lkrlsp3  37962  lkrshp  37963  lkrshp3  37964  lkrshpor  37965  lkrshp4  37966  lshpsmreu  37967  lshpkrlem1  37968  lshpkrlem4  37971  lshpkrlem5  37972  lshpkrlem6  37973  lshpkr  37975  lshpkrex  37976  lfl1dim  37979  lfl1dim2N  37980  lduallvec  38012  lduallkr3  38020  lkrpssN  38021  ldual1dim  38024  lkrss2N  38027  lkreqN  38028  lkrlspeqN  38029  dva0g  39886  dia1dim2  39921  dia1dimid  39922  dia2dimlem5  39927  dia2dimlem7  39929  dia2dimlem9  39931  dia2dimlem10  39932  dia2dimlem13  39935  dvhlmod  39969  diblsmopel  40030  lclkrlem2m  40378  lclkrlem2n  40379  lcfrlem1  40401  lcfrlem2  40402  lcfrlem3  40403  lcdlmod  40451  baerlem3lem1  40566  baerlem5alem1  40567  baerlem5blem1  40568  baerlem3lem2  40569  baerlem5alem2  40570  baerlem5blem2  40571  baerlem5amN  40575  baerlem5bmN  40576  baerlem5abmN  40577  mapdindp0  40578  mapdindp1  40579  mapdindp2  40580  mapdindp3  40581  mapdindp4  40582  lspindp5  40629  lvecgrp  41103  lvecring  41105  prjspersym  41345  prjsper  41346  prjspreln0  41347  prjspvs  41348  prjspeclsp  41350  0prjspn  41366  lincreslvec3  47116  isldepslvec2  47119  lindssnlvec  47120  lvecpsslmod  47141