Theorem lveclmod 19871

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6324  Scalarcsca 16560  DivRingcdr 19495  LModclmod 19627  LVecclvec 19867

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-lvec 19868

This theorem is referenced by:  lsslvec  19872  lvecvs0or  19873  lssvs0or  19875  lvecvscan  19876  lvecvscan2  19877  lvecinv  19878  lspsnvs  19879  lspsneleq  19880  lspsncmp  19881  lspsnne1  19882  lspsnnecom  19884  lspabs2  19885  lspabs3  19886  lspsneq  19887  lspsnel4  19889  lspdisj  19890  lspdisjb  19891  lspdisj2  19892  lspfixed  19893  lspexch  19894  lspexchn1  19895  lspindpi  19897  lvecindp  19903  lvecindp2  19904  lsmcv  19906  lspsolv  19908  lssacsex  19909  lspsnat  19910  lsppratlem2  19913  lsppratlem3  19914  lsppratlem4  19915  lsppratlem6  19917  lspprat  19918  islbs2  19919  islbs3  19920  lbsacsbs  19921  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  phllmod  20319  isphld  20343  islinds4  20524  lvecisfrlm  20532  cvsi  23735  0nellinds  30986  lindssn  30993  linds2eq  30995  lvecdim0i  31092  lssdimle  31094  tngdim  31099  matdim  31101  lbslsat  31102  lsatdim  31103  drngdimgt0  31104  lindsunlem  31108  lindsun  31109  lbsdiflsp0  31110  dimkerim  31111  qusdimsum  31112  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  extdg1id  31141  ccfldextdgrr  31145  lindsadd  35050  lshpnelb  36280  lshpnel2N  36281  lshpdisj  36283  lshpcmp  36284  lsatcmp  36299  lsatcmp2  36300  lsatel  36301  lsatelbN  36302  lsatfixedN  36305  lsmcv2  36325  lsatcv0  36327  lsatcveq0  36328  lsat0cv  36329  lcvp  36336  lcv1  36337  lcv2  36338  lsatexch  36339  lsatnem0  36341  lsatexch1  36342  lsatcv0eq  36343  lsatcv1  36344  lsatcvatlem  36345  lsatcvat  36346  lsatcvat2  36347  lsatcvat3  36348  islshpcv  36349  l1cvpat  36350  l1cvat  36351  lfl1  36366  lkrsc  36393  lkrscss  36394  eqlkr  36395  eqlkr3  36397  lkrlsp  36398  lkrlsp3  36400  lkrshp  36401  lkrshp3  36402  lkrshpor  36403  lkrshp4  36404  lshpsmreu  36405  lshpkrlem1  36406  lshpkrlem4  36409  lshpkrlem5  36410  lshpkrlem6  36411  lshpkr  36413  lshpkrex  36414  lfl1dim  36417  lfl1dim2N  36418  lduallvec  36450  lduallkr3  36458  lkrpssN  36459  ldual1dim  36462  lkrss2N  36465  lkreqN  36466  lkrlspeqN  36467  dva0g  38323  dia1dim2  38358  dia1dimid  38359  dia2dimlem5  38364  dia2dimlem7  38366  dia2dimlem9  38368  dia2dimlem10  38369  dia2dimlem13  38372  dvhlmod  38406  diblsmopel  38467  lclkrlem2m  38815  lclkrlem2n  38816  lcfrlem1  38838  lcfrlem2  38839  lcfrlem3  38840  lcdlmod  38888  baerlem3lem1  39003  baerlem5alem1  39004  baerlem5blem1  39005  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  baerlem5amN  39012  baerlem5bmN  39013  baerlem5abmN  39014  mapdindp0  39015  mapdindp1  39016  mapdindp2  39017  mapdindp3  39018  mapdindp4  39019  lspindp5  39066  lvecgrp  39448  lveclmodd  39449  lvecring  39451  prjspersym  39601  prjsper  39602  prjspreln0  39603  prjspvs  39604  prjspeclsp  39606  0prjspn  39614  lincreslvec3  44891  isldepslvec2  44894  lindssnlvec  44895  lvecpsslmod  44916