Theorem lveclmod 21206

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

Syntax hints:   → wi 4   ∈ wcel 2141  ‘cfv 6536  Scalarcsca 17312  DivRingcdr 20812  LModclmod 20960  LVecclvec 21202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-lvec 21203

This theorem is referenced by:  lveclmodd  21207  lsslvec  21209  lvecvs0or  21211  lssvs0or  21213  lvecvscan  21214  lvecvscan2  21215  lvecinv  21216  lspsnvs  21217  lspsneleq  21218  lspsncmp  21219  lspsnne1  21220  lspsnnecom  21222  lspabs2  21223  lspabs3  21224  lspsneq  21225  ellspsn4  21227  lspdisj  21228  lspdisjb  21229  lspdisj2  21230  lspfixed  21231  lspexch  21232  lspexchn1  21233  lspindpi  21235  lvecindp  21241  lvecindp2  21242  lsmcv  21244  lspsolv  21246  lssacsex  21247  lspsnat  21248  lsppratlem2  21251  lsppratlem3  21252  lsppratlem4  21253  lsppratlem6  21255  lspprat  21256  islbs2  21257  islbs3  21258  lbsacsbs  21259  lbsextlem2  21262  lbsextlem3  21263  lbsextlem4  21264  phllmod  21759  isphld  21783  islinds4  21964  lvecisfrlm  21972  cvsi  25268  0nellinds  33651  lindssn  33657  linds2eq  33660  exsslsb  33953  lvecdim0i  33962  lssdimle  33964  tngdim  33969  matdim  33971  lbslsat  33972  lsatdim  33973  drngdimgt0  33974  lindsunlem  33980  lindsun  33981  lbsdiflsp0  33982  dimkerim  33983  qusdimsum  33984  fedgmullem1  33985  fedgmullem2  33986  fedgmul  33987  extdg1id  34022  ccfldextdgrr  34028  lindsadd  38230  lshpnelb  39726  lshpnel2N  39727  lshpdisj  39729  lshpcmp  39730  lsatcmp  39745  lsatcmp2  39746  lsatel  39747  lsatelbN  39748  lsatfixedN  39751  lsmcv2  39771  lsatcv0  39773  lsatcveq0  39774  lsat0cv  39775  lcvp  39782  lcv1  39783  lcv2  39784  lsatexch  39785  lsatnem0  39787  lsatexch1  39788  lsatcv0eq  39789  lsatcv1  39790  lsatcvatlem  39791  lsatcvat  39792  lsatcvat2  39793  lsatcvat3  39794  islshpcv  39795  l1cvpat  39796  l1cvat  39797  lfl1  39812  lkrsc  39839  lkrscss  39840  eqlkr  39841  eqlkr3  39843  lkrlsp  39844  lkrlsp3  39846  lkrshp  39847  lkrshp3  39848  lkrshpor  39849  lkrshp4  39850  lshpsmreu  39851  lshpkrlem1  39852  lshpkrlem4  39855  lshpkrlem5  39856  lshpkrlem6  39857  lshpkr  39859  lshpkrex  39860  lfl1dim  39863  lfl1dim2N  39864  lduallvec  39896  lduallkr3  39904  lkrpssN  39905  ldual1dim  39908  lkrss2N  39911  lkreqN  39912  lkrlspeqN  39913  dva0g  41769  dia1dim2  41804  dia1dimid  41805  dia2dimlem5  41810  dia2dimlem7  41812  dia2dimlem9  41814  dia2dimlem10  41815  dia2dimlem13  41818  dvhlmod  41852  diblsmopel  41913  lclkrlem2m  42261  lclkrlem2n  42262  lcfrlem1  42284  lcfrlem2  42285  lcfrlem3  42286  lcdlmod  42334  baerlem3lem1  42449  baerlem5alem1  42450  baerlem5blem1  42451  baerlem3lem2  42452  baerlem5alem2  42453  baerlem5blem2  42454  baerlem5amN  42458  baerlem5bmN  42459  baerlem5abmN  42460  mapdindp0  42461  mapdindp1  42462  mapdindp2  42463  mapdindp3  42464  mapdindp4  42465  lspindp5  42512  lvecgrp  43275  lvecring  43276  prjspersym  43309  prjsper  43310  prjspreln0  43311  prjspvs  43312  prjspeclsp  43314  0prjspn  43330  lincreslvec3  49229  isldepslvec2  49232  lindssnlvec  49233  lvecpsslmod  49254