Theorem lveclmod 21146

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

Syntax hints:   → wi 4   ∈ wcel 2136  ‘cfv 6510  Scalarcsca 17265  DivRingcdr 20751  LModclmod 20900  LVecclvec 21142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-lvec 21143

This theorem is referenced by:  lveclmodd  21147  lsslvec  21149  lvecvs0or  21151  lssvs0or  21153  lvecvscan  21154  lvecvscan2  21155  lvecinv  21156  lspsnvs  21157  lspsneleq  21158  lspsncmp  21159  lspsnne1  21160  lspsnnecom  21162  lspabs2  21163  lspabs3  21164  lspsneq  21165  ellspsn4  21167  lspdisj  21168  lspdisjb  21169  lspdisj2  21170  lspfixed  21171  lspexch  21172  lspexchn1  21173  lspindpi  21175  lvecindp  21181  lvecindp2  21182  lsmcv  21184  lspsolv  21186  lssacsex  21187  lspsnat  21188  lsppratlem2  21191  lsppratlem3  21192  lsppratlem4  21193  lsppratlem6  21195  lspprat  21196  islbs2  21197  islbs3  21198  lbsacsbs  21199  lbsextlem2  21202  lbsextlem3  21203  lbsextlem4  21204  phllmod  21655  isphld  21679  islinds4  21860  lvecisfrlm  21868  cvsi  25165  0nellinds  33510  lindssn  33518  linds2eq  33521  exsslsb  33848  lvecdim0i  33857  lssdimle  33859  tngdim  33864  matdim  33866  lbslsat  33867  lsatdim  33868  drngdimgt0  33869  lindsunlem  33875  lindsun  33876  lbsdiflsp0  33877  dimkerim  33878  qusdimsum  33879  fedgmullem1  33880  fedgmullem2  33881  fedgmul  33882  extdg1id  33917  ccfldextdgrr  33923  lindsadd  38060  lshpnelb  39556  lshpnel2N  39557  lshpdisj  39559  lshpcmp  39560  lsatcmp  39575  lsatcmp2  39576  lsatel  39577  lsatelbN  39578  lsatfixedN  39581  lsmcv2  39601  lsatcv0  39603  lsatcveq0  39604  lsat0cv  39605  lcvp  39612  lcv1  39613  lcv2  39614  lsatexch  39615  lsatnem0  39617  lsatexch1  39618  lsatcv0eq  39619  lsatcv1  39620  lsatcvatlem  39621  lsatcvat  39622  lsatcvat2  39623  lsatcvat3  39624  islshpcv  39625  l1cvpat  39626  l1cvat  39627  lfl1  39642  lkrsc  39669  lkrscss  39670  eqlkr  39671  eqlkr3  39673  lkrlsp  39674  lkrlsp3  39676  lkrshp  39677  lkrshp3  39678  lkrshpor  39679  lkrshp4  39680  lshpsmreu  39681  lshpkrlem1  39682  lshpkrlem4  39685  lshpkrlem5  39686  lshpkrlem6  39687  lshpkr  39689  lshpkrex  39690  lfl1dim  39693  lfl1dim2N  39694  lduallvec  39726  lduallkr3  39734  lkrpssN  39735  ldual1dim  39738  lkrss2N  39741  lkreqN  39742  lkrlspeqN  39743  dva0g  41599  dia1dim2  41634  dia1dimid  41635  dia2dimlem5  41640  dia2dimlem7  41642  dia2dimlem9  41644  dia2dimlem10  41645  dia2dimlem13  41648  dvhlmod  41682  diblsmopel  41743  lclkrlem2m  42091  lclkrlem2n  42092  lcfrlem1  42114  lcfrlem2  42115  lcfrlem3  42116  lcdlmod  42164  baerlem3lem1  42279  baerlem5alem1  42280  baerlem5blem1  42281  baerlem3lem2  42282  baerlem5alem2  42283  baerlem5blem2  42284  baerlem5amN  42288  baerlem5bmN  42289  baerlem5abmN  42290  mapdindp0  42291  mapdindp1  42292  mapdindp2  42293  mapdindp3  42294  mapdindp4  42295  lspindp5  42342  lvecgrp  43103  lvecring  43104  prjspersym  43137  prjsper  43138  prjspreln0  43139  prjspvs  43140  prjspeclsp  43142  0prjspn  43158  lincreslvec3  49052  isldepslvec2  49055  lindssnlvec  49056  lvecpsslmod  49077