Theorem lveclmod 19878

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6355  Scalarcsca 16568  DivRingcdr 19502  LModclmod 19634  LVecclvec 19874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-lvec 19875

This theorem is referenced by:  lsslvec  19879  lvecvs0or  19880  lssvs0or  19882  lvecvscan  19883  lvecvscan2  19884  lvecinv  19885  lspsnvs  19886  lspsneleq  19887  lspsncmp  19888  lspsnne1  19889  lspsnnecom  19891  lspabs2  19892  lspabs3  19893  lspsneq  19894  lspsnel4  19896  lspdisj  19897  lspdisjb  19898  lspdisj2  19899  lspfixed  19900  lspexch  19901  lspexchn1  19902  lspindpi  19904  lvecindp  19910  lvecindp2  19911  lsmcv  19913  lspsolv  19915  lssacsex  19916  lspsnat  19917  lsppratlem2  19920  lsppratlem3  19921  lsppratlem4  19922  lsppratlem6  19924  lspprat  19925  islbs2  19926  islbs3  19927  lbsacsbs  19928  lbsextlem2  19931  lbsextlem3  19932  lbsextlem4  19933  phllmod  20774  isphld  20798  islinds4  20979  lvecisfrlm  20987  cvsi  23734  0nellinds  30935  lindssn  30939  linds2eq  30941  lvecdim0i  31004  lssdimle  31006  tngdim  31011  matdim  31013  lbslsat  31014  lsatdim  31015  drngdimgt0  31016  lindsunlem  31020  lindsun  31021  lbsdiflsp0  31022  dimkerim  31023  qusdimsum  31024  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  extdg1id  31053  ccfldextdgrr  31057  lindsadd  34900  lshpnelb  36135  lshpnel2N  36136  lshpdisj  36138  lshpcmp  36139  lsatcmp  36154  lsatcmp2  36155  lsatel  36156  lsatelbN  36157  lsatfixedN  36160  lsmcv2  36180  lsatcv0  36182  lsatcveq0  36183  lsat0cv  36184  lcvp  36191  lcv1  36192  lcv2  36193  lsatexch  36194  lsatnem0  36196  lsatexch1  36197  lsatcv0eq  36198  lsatcv1  36199  lsatcvatlem  36200  lsatcvat  36201  lsatcvat2  36202  lsatcvat3  36203  islshpcv  36204  l1cvpat  36205  l1cvat  36206  lfl1  36221  lkrsc  36248  lkrscss  36249  eqlkr  36250  eqlkr3  36252  lkrlsp  36253  lkrlsp3  36255  lkrshp  36256  lkrshp3  36257  lkrshpor  36258  lkrshp4  36259  lshpsmreu  36260  lshpkrlem1  36261  lshpkrlem4  36264  lshpkrlem5  36265  lshpkrlem6  36266  lshpkr  36268  lshpkrex  36269  lfl1dim  36272  lfl1dim2N  36273  lduallvec  36305  lduallkr3  36313  lkrpssN  36314  ldual1dim  36317  lkrss2N  36320  lkreqN  36321  lkrlspeqN  36322  dva0g  38178  dia1dim2  38213  dia1dimid  38214  dia2dimlem5  38219  dia2dimlem7  38221  dia2dimlem9  38223  dia2dimlem10  38224  dia2dimlem13  38227  dvhlmod  38261  diblsmopel  38322  lclkrlem2m  38670  lclkrlem2n  38671  lcfrlem1  38693  lcfrlem2  38694  lcfrlem3  38695  lcdlmod  38743  baerlem3lem1  38858  baerlem5alem1  38859  baerlem5blem1  38860  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  baerlem5amN  38867  baerlem5bmN  38868  baerlem5abmN  38869  mapdindp0  38870  mapdindp1  38871  mapdindp2  38872  mapdindp3  38873  mapdindp4  38874  lspindp5  38921  lvecgrp  39166  lvecring  39167  prjspersym  39277  prjsper  39278  prjspreln0  39279  prjspvs  39280  prjspeclsp  39282  0prjspn  39290  lincreslvec3  44557  isldepslvec2  44560  lindssnlvec  44561  lvecpsslmod  44582