Theorem lveclmod 21062

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  Scalarcsca 17184  DivRingcdr 20666  LModclmod 20815  LVecclvec 21058

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-lvec 21059

This theorem is referenced by:  lveclmodd  21063  lsslvec  21065  lvecvs0or  21067  lssvs0or  21069  lvecvscan  21070  lvecvscan2  21071  lvecinv  21072  lspsnvs  21073  lspsneleq  21074  lspsncmp  21075  lspsnne1  21076  lspsnnecom  21078  lspabs2  21079  lspabs3  21080  lspsneq  21081  ellspsn4  21083  lspdisj  21084  lspdisjb  21085  lspdisj2  21086  lspfixed  21087  lspexch  21088  lspexchn1  21089  lspindpi  21091  lvecindp  21097  lvecindp2  21098  lsmcv  21100  lspsolv  21102  lssacsex  21103  lspsnat  21104  lsppratlem2  21107  lsppratlem3  21108  lsppratlem4  21109  lsppratlem6  21111  lspprat  21112  islbs2  21113  islbs3  21114  lbsacsbs  21115  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  phllmod  21589  isphld  21613  islinds4  21794  lvecisfrlm  21802  cvsi  25090  0nellinds  33432  lindssn  33440  linds2eq  33443  exsslsb  33734  lvecdim0i  33743  lssdimle  33745  tngdim  33751  matdim  33753  lbslsat  33754  lsatdim  33755  drngdimgt0  33756  lindsunlem  33762  lindsun  33763  lbsdiflsp0  33764  dimkerim  33765  qusdimsum  33766  fedgmullem1  33767  fedgmullem2  33768  fedgmul  33769  extdg1id  33804  ccfldextdgrr  33810  lindsadd  37785  lshpnelb  39281  lshpnel2N  39282  lshpdisj  39284  lshpcmp  39285  lsatcmp  39300  lsatcmp2  39301  lsatel  39302  lsatelbN  39303  lsatfixedN  39306  lsmcv2  39326  lsatcv0  39328  lsatcveq0  39329  lsat0cv  39330  lcvp  39337  lcv1  39338  lcv2  39339  lsatexch  39340  lsatnem0  39342  lsatexch1  39343  lsatcv0eq  39344  lsatcv1  39345  lsatcvatlem  39346  lsatcvat  39347  lsatcvat2  39348  lsatcvat3  39349  islshpcv  39350  l1cvpat  39351  l1cvat  39352  lfl1  39367  lkrsc  39394  lkrscss  39395  eqlkr  39396  eqlkr3  39398  lkrlsp  39399  lkrlsp3  39401  lkrshp  39402  lkrshp3  39403  lkrshpor  39404  lkrshp4  39405  lshpsmreu  39406  lshpkrlem1  39407  lshpkrlem4  39410  lshpkrlem5  39411  lshpkrlem6  39412  lshpkr  39414  lshpkrex  39415  lfl1dim  39418  lfl1dim2N  39419  lduallvec  39451  lduallkr3  39459  lkrpssN  39460  ldual1dim  39463  lkrss2N  39466  lkreqN  39467  lkrlspeqN  39468  dva0g  41324  dia1dim2  41359  dia1dimid  41360  dia2dimlem5  41365  dia2dimlem7  41367  dia2dimlem9  41369  dia2dimlem10  41370  dia2dimlem13  41373  dvhlmod  41407  diblsmopel  41468  lclkrlem2m  41816  lclkrlem2n  41817  lcfrlem1  41839  lcfrlem2  41840  lcfrlem3  41841  lcdlmod  41889  baerlem3lem1  42004  baerlem5alem1  42005  baerlem5blem1  42006  baerlem3lem2  42007  baerlem5alem2  42008  baerlem5blem2  42009  baerlem5amN  42013  baerlem5bmN  42014  baerlem5abmN  42015  mapdindp0  42016  mapdindp1  42017  mapdindp2  42018  mapdindp3  42019  mapdindp4  42020  lspindp5  42067  lvecgrp  42828  lvecring  42829  prjspersym  42886  prjsper  42887  prjspreln0  42888  prjspvs  42889  prjspeclsp  42891  0prjspn  42907  lincreslvec3  48764  isldepslvec2  48767  lindssnlvec  48768  lvecpsslmod  48789