Theorem lveclmod 21103

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

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6492  Scalarcsca 17221  DivRingcdr 20708  LModclmod 20857  LVecclvec 21099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-lvec 21100

This theorem is referenced by:  lveclmodd  21104  lsslvec  21106  lvecvs0or  21108  lssvs0or  21110  lvecvscan  21111  lvecvscan2  21112  lvecinv  21113  lspsnvs  21114  lspsneleq  21115  lspsncmp  21116  lspsnne1  21117  lspsnnecom  21119  lspabs2  21120  lspabs3  21121  lspsneq  21122  ellspsn4  21124  lspdisj  21125  lspdisjb  21126  lspdisj2  21127  lspfixed  21128  lspexch  21129  lspexchn1  21130  lspindpi  21132  lvecindp  21138  lvecindp2  21139  lsmcv  21141  lspsolv  21143  lssacsex  21144  lspsnat  21145  lsppratlem2  21148  lsppratlem3  21149  lsppratlem4  21150  lsppratlem6  21152  lspprat  21153  islbs2  21154  islbs3  21155  lbsacsbs  21156  lbsextlem2  21159  lbsextlem3  21160  lbsextlem4  21161  phllmod  21612  isphld  21636  islinds4  21817  lvecisfrlm  21825  cvsi  25122  0nellinds  33460  lindssn  33468  linds2eq  33471  exsslsb  33788  lvecdim0i  33797  lssdimle  33799  tngdim  33804  matdim  33806  lbslsat  33807  lsatdim  33808  drngdimgt0  33809  lindsunlem  33815  lindsun  33816  lbsdiflsp0  33817  dimkerim  33818  qusdimsum  33819  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  extdg1id  33857  ccfldextdgrr  33863  lindsadd  37981  lshpnelb  39477  lshpnel2N  39478  lshpdisj  39480  lshpcmp  39481  lsatcmp  39496  lsatcmp2  39497  lsatel  39498  lsatelbN  39499  lsatfixedN  39502  lsmcv2  39522  lsatcv0  39524  lsatcveq0  39525  lsat0cv  39526  lcvp  39533  lcv1  39534  lcv2  39535  lsatexch  39536  lsatnem0  39538  lsatexch1  39539  lsatcv0eq  39540  lsatcv1  39541  lsatcvatlem  39542  lsatcvat  39543  lsatcvat2  39544  lsatcvat3  39545  islshpcv  39546  l1cvpat  39547  l1cvat  39548  lfl1  39563  lkrsc  39590  lkrscss  39591  eqlkr  39592  eqlkr3  39594  lkrlsp  39595  lkrlsp3  39597  lkrshp  39598  lkrshp3  39599  lkrshpor  39600  lkrshp4  39601  lshpsmreu  39602  lshpkrlem1  39603  lshpkrlem4  39606  lshpkrlem5  39607  lshpkrlem6  39608  lshpkr  39610  lshpkrex  39611  lfl1dim  39614  lfl1dim2N  39615  lduallvec  39647  lduallkr3  39655  lkrpssN  39656  ldual1dim  39659  lkrss2N  39662  lkreqN  39663  lkrlspeqN  39664  dva0g  41520  dia1dim2  41555  dia1dimid  41556  dia2dimlem5  41561  dia2dimlem7  41563  dia2dimlem9  41565  dia2dimlem10  41566  dia2dimlem13  41569  dvhlmod  41603  diblsmopel  41664  lclkrlem2m  42012  lclkrlem2n  42013  lcfrlem1  42035  lcfrlem2  42036  lcfrlem3  42037  lcdlmod  42085  baerlem3lem1  42200  baerlem5alem1  42201  baerlem5blem1  42202  baerlem3lem2  42203  baerlem5alem2  42204  baerlem5blem2  42205  baerlem5amN  42209  baerlem5bmN  42210  baerlem5abmN  42211  mapdindp0  42212  mapdindp1  42213  mapdindp2  42214  mapdindp3  42215  mapdindp4  42216  lspindp5  42263  lvecgrp  43024  lvecring  43025  prjspersym  43058  prjsper  43059  prjspreln0  43060  prjspvs  43061  prjspeclsp  43063  0prjspn  43079  lincreslvec3  48974  isldepslvec2  48977  lindssnlvec  48978  lvecpsslmod  48999