Theorem lveclmod 21101

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6499  Scalarcsca 17223  DivRingcdr 20706  LModclmod 20855  LVecclvec 21097

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 6455  df-fv 6507  df-lvec 21098

This theorem is referenced by:  lveclmodd  21102  lsslvec  21104  lvecvs0or  21106  lssvs0or  21108  lvecvscan  21109  lvecvscan2  21110  lvecinv  21111  lspsnvs  21112  lspsneleq  21113  lspsncmp  21114  lspsnne1  21115  lspsnnecom  21117  lspabs2  21118  lspabs3  21119  lspsneq  21120  ellspsn4  21122  lspdisj  21123  lspdisjb  21124  lspdisj2  21125  lspfixed  21126  lspexch  21127  lspexchn1  21128  lspindpi  21130  lvecindp  21136  lvecindp2  21137  lsmcv  21139  lspsolv  21141  lssacsex  21142  lspsnat  21143  lsppratlem2  21146  lsppratlem3  21147  lsppratlem4  21148  lsppratlem6  21150  lspprat  21151  islbs2  21152  islbs3  21153  lbsacsbs  21154  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  phllmod  21610  isphld  21634  islinds4  21815  lvecisfrlm  21823  cvsi  25097  0nellinds  33430  lindssn  33438  linds2eq  33441  exsslsb  33741  lvecdim0i  33750  lssdimle  33752  tngdim  33757  matdim  33759  lbslsat  33760  lsatdim  33761  drngdimgt0  33762  lindsunlem  33768  lindsun  33769  lbsdiflsp0  33770  dimkerim  33771  qusdimsum  33772  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  extdg1id  33810  ccfldextdgrr  33816  lindsadd  37934  lshpnelb  39430  lshpnel2N  39431  lshpdisj  39433  lshpcmp  39434  lsatcmp  39449  lsatcmp2  39450  lsatel  39451  lsatelbN  39452  lsatfixedN  39455  lsmcv2  39475  lsatcv0  39477  lsatcveq0  39478  lsat0cv  39479  lcvp  39486  lcv1  39487  lcv2  39488  lsatexch  39489  lsatnem0  39491  lsatexch1  39492  lsatcv0eq  39493  lsatcv1  39494  lsatcvatlem  39495  lsatcvat  39496  lsatcvat2  39497  lsatcvat3  39498  islshpcv  39499  l1cvpat  39500  l1cvat  39501  lfl1  39516  lkrsc  39543  lkrscss  39544  eqlkr  39545  eqlkr3  39547  lkrlsp  39548  lkrlsp3  39550  lkrshp  39551  lkrshp3  39552  lkrshpor  39553  lkrshp4  39554  lshpsmreu  39555  lshpkrlem1  39556  lshpkrlem4  39559  lshpkrlem5  39560  lshpkrlem6  39561  lshpkr  39563  lshpkrex  39564  lfl1dim  39567  lfl1dim2N  39568  lduallvec  39600  lduallkr3  39608  lkrpssN  39609  ldual1dim  39612  lkrss2N  39615  lkreqN  39616  lkrlspeqN  39617  dva0g  41473  dia1dim2  41508  dia1dimid  41509  dia2dimlem5  41514  dia2dimlem7  41516  dia2dimlem9  41518  dia2dimlem10  41519  dia2dimlem13  41522  dvhlmod  41556  diblsmopel  41617  lclkrlem2m  41965  lclkrlem2n  41966  lcfrlem1  41988  lcfrlem2  41989  lcfrlem3  41990  lcdlmod  42038  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdindp0  42165  mapdindp1  42166  mapdindp2  42167  mapdindp3  42168  mapdindp4  42169  lspindp5  42216  lvecgrp  42982  lvecring  42983  prjspersym  43040  prjsper  43041  prjspreln0  43042  prjspvs  43043  prjspeclsp  43045  0prjspn  43061  lincreslvec3  48952  isldepslvec2  48955  lindssnlvec  48956  lvecpsslmod  48977