Theorem lveclmod 20861

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

Syntax hints:   → wi 4   ∈ wcel 2104  ‘cfv 6542  Scalarcsca 17204  DivRingcdr 20500  LModclmod 20614  LVecclvec 20857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-lvec 20858

This theorem is referenced by:  lveclmodd  20862  lsslvec  20864  lvecvs0or  20866  lssvs0or  20868  lvecvscan  20869  lvecvscan2  20870  lvecinv  20871  lspsnvs  20872  lspsneleq  20873  lspsncmp  20874  lspsnne1  20875  lspsnnecom  20877  lspabs2  20878  lspabs3  20879  lspsneq  20880  lspsnel4  20882  lspdisj  20883  lspdisjb  20884  lspdisj2  20885  lspfixed  20886  lspexch  20887  lspexchn1  20888  lspindpi  20890  lvecindp  20896  lvecindp2  20897  lsmcv  20899  lspsolv  20901  lssacsex  20902  lspsnat  20903  lsppratlem2  20906  lsppratlem3  20907  lsppratlem4  20908  lsppratlem6  20910  lspprat  20911  islbs2  20912  islbs3  20913  lbsacsbs  20914  lbsextlem2  20917  lbsextlem3  20918  lbsextlem4  20919  phllmod  21402  isphld  21426  islinds4  21609  lvecisfrlm  21617  cvsi  24877  0nellinds  32757  lindssn  32768  linds2eq  32771  lvecdim0i  32978  lssdimle  32980  tngdim  32986  matdim  32988  lbslsat  32989  lsatdim  32990  drngdimgt0  32991  lindsunlem  32997  lindsun  32998  lbsdiflsp0  32999  dimkerim  33000  qusdimsum  33001  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  extdg1id  33030  ccfldextdgrr  33035  lindsadd  36784  lshpnelb  38157  lshpnel2N  38158  lshpdisj  38160  lshpcmp  38161  lsatcmp  38176  lsatcmp2  38177  lsatel  38178  lsatelbN  38179  lsatfixedN  38182  lsmcv2  38202  lsatcv0  38204  lsatcveq0  38205  lsat0cv  38206  lcvp  38213  lcv1  38214  lcv2  38215  lsatexch  38216  lsatnem0  38218  lsatexch1  38219  lsatcv0eq  38220  lsatcv1  38221  lsatcvatlem  38222  lsatcvat  38223  lsatcvat2  38224  lsatcvat3  38225  islshpcv  38226  l1cvpat  38227  l1cvat  38228  lfl1  38243  lkrsc  38270  lkrscss  38271  eqlkr  38272  eqlkr3  38274  lkrlsp  38275  lkrlsp3  38277  lkrshp  38278  lkrshp3  38279  lkrshpor  38280  lkrshp4  38281  lshpsmreu  38282  lshpkrlem1  38283  lshpkrlem4  38286  lshpkrlem5  38287  lshpkrlem6  38288  lshpkr  38290  lshpkrex  38291  lfl1dim  38294  lfl1dim2N  38295  lduallvec  38327  lduallkr3  38335  lkrpssN  38336  ldual1dim  38339  lkrss2N  38342  lkreqN  38343  lkrlspeqN  38344  dva0g  40201  dia1dim2  40236  dia1dimid  40237  dia2dimlem5  40242  dia2dimlem7  40244  dia2dimlem9  40246  dia2dimlem10  40247  dia2dimlem13  40250  dvhlmod  40284  diblsmopel  40345  lclkrlem2m  40693  lclkrlem2n  40694  lcfrlem1  40716  lcfrlem2  40717  lcfrlem3  40718  lcdlmod  40766  baerlem3lem1  40881  baerlem5alem1  40882  baerlem5blem1  40883  baerlem3lem2  40884  baerlem5alem2  40885  baerlem5blem2  40886  baerlem5amN  40890  baerlem5bmN  40891  baerlem5abmN  40892  mapdindp0  40893  mapdindp1  40894  mapdindp2  40895  mapdindp3  40896  mapdindp4  40897  lspindp5  40944  lvecgrp  41409  lvecring  41410  prjspersym  41651  prjsper  41652  prjspreln0  41653  prjspvs  41654  prjspeclsp  41656  0prjspn  41672  lincreslvec3  47250  isldepslvec2  47253  lindssnlvec  47254  lvecpsslmod  47275