Theorem lveclmod 21091

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6490  Scalarcsca 17212  DivRingcdr 20695  LModclmod 20844  LVecclvec 21087

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-lvec 21088

This theorem is referenced by:  lveclmodd  21092  lsslvec  21094  lvecvs0or  21096  lssvs0or  21098  lvecvscan  21099  lvecvscan2  21100  lvecinv  21101  lspsnvs  21102  lspsneleq  21103  lspsncmp  21104  lspsnne1  21105  lspsnnecom  21107  lspabs2  21108  lspabs3  21109  lspsneq  21110  ellspsn4  21112  lspdisj  21113  lspdisjb  21114  lspdisj2  21115  lspfixed  21116  lspexch  21117  lspexchn1  21118  lspindpi  21120  lvecindp  21126  lvecindp2  21127  lsmcv  21129  lspsolv  21131  lssacsex  21132  lspsnat  21133  lsppratlem2  21136  lsppratlem3  21137  lsppratlem4  21138  lsppratlem6  21140  lspprat  21141  islbs2  21142  islbs3  21143  lbsacsbs  21144  lbsextlem2  21147  lbsextlem3  21148  lbsextlem4  21149  phllmod  21618  isphld  21642  islinds4  21823  lvecisfrlm  21831  cvsi  25106  0nellinds  33450  lindssn  33458  linds2eq  33461  exsslsb  33761  lvecdim0i  33770  lssdimle  33772  tngdim  33778  matdim  33780  lbslsat  33781  lsatdim  33782  drngdimgt0  33783  lindsunlem  33789  lindsun  33790  lbsdiflsp0  33791  dimkerim  33792  qusdimsum  33793  fedgmullem1  33794  fedgmullem2  33795  fedgmul  33796  extdg1id  33831  ccfldextdgrr  33837  lindsadd  37945  lshpnelb  39441  lshpnel2N  39442  lshpdisj  39444  lshpcmp  39445  lsatcmp  39460  lsatcmp2  39461  lsatel  39462  lsatelbN  39463  lsatfixedN  39466  lsmcv2  39486  lsatcv0  39488  lsatcveq0  39489  lsat0cv  39490  lcvp  39497  lcv1  39498  lcv2  39499  lsatexch  39500  lsatnem0  39502  lsatexch1  39503  lsatcv0eq  39504  lsatcv1  39505  lsatcvatlem  39506  lsatcvat  39507  lsatcvat2  39508  lsatcvat3  39509  islshpcv  39510  l1cvpat  39511  l1cvat  39512  lfl1  39527  lkrsc  39554  lkrscss  39555  eqlkr  39556  eqlkr3  39558  lkrlsp  39559  lkrlsp3  39561  lkrshp  39562  lkrshp3  39563  lkrshpor  39564  lkrshp4  39565  lshpsmreu  39566  lshpkrlem1  39567  lshpkrlem4  39570  lshpkrlem5  39571  lshpkrlem6  39572  lshpkr  39574  lshpkrex  39575  lfl1dim  39578  lfl1dim2N  39579  lduallvec  39611  lduallkr3  39619  lkrpssN  39620  ldual1dim  39623  lkrss2N  39626  lkreqN  39627  lkrlspeqN  39628  dva0g  41484  dia1dim2  41519  dia1dimid  41520  dia2dimlem5  41525  dia2dimlem7  41527  dia2dimlem9  41529  dia2dimlem10  41530  dia2dimlem13  41533  dvhlmod  41567  diblsmopel  41628  lclkrlem2m  41976  lclkrlem2n  41977  lcfrlem1  41999  lcfrlem2  42000  lcfrlem3  42001  lcdlmod  42049  baerlem3lem1  42164  baerlem5alem1  42165  baerlem5blem1  42166  baerlem3lem2  42167  baerlem5alem2  42168  baerlem5blem2  42169  baerlem5amN  42173  baerlem5bmN  42174  baerlem5abmN  42175  mapdindp0  42176  mapdindp1  42177  mapdindp2  42178  mapdindp3  42179  mapdindp4  42180  lspindp5  42227  lvecgrp  42993  lvecring  42994  prjspersym  43051  prjsper  43052  prjspreln0  43053  prjspvs  43054  prjspeclsp  43056  0prjspn  43072  lincreslvec3  48955  isldepslvec2  48958  lindssnlvec  48959  lvecpsslmod  48980