Theorem lveclmod 21020

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  Scalarcsca 17230  DivRingcdr 20645  LModclmod 20773  LVecclvec 21016

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-lvec 21017

This theorem is referenced by:  lveclmodd  21021  lsslvec  21023  lvecvs0or  21025  lssvs0or  21027  lvecvscan  21028  lvecvscan2  21029  lvecinv  21030  lspsnvs  21031  lspsneleq  21032  lspsncmp  21033  lspsnne1  21034  lspsnnecom  21036  lspabs2  21037  lspabs3  21038  lspsneq  21039  ellspsn4  21041  lspdisj  21042  lspdisjb  21043  lspdisj2  21044  lspfixed  21045  lspexch  21046  lspexchn1  21047  lspindpi  21049  lvecindp  21055  lvecindp2  21056  lsmcv  21058  lspsolv  21060  lssacsex  21061  lspsnat  21062  lsppratlem2  21065  lsppratlem3  21066  lsppratlem4  21067  lsppratlem6  21069  lspprat  21070  islbs2  21071  islbs3  21072  lbsacsbs  21073  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  phllmod  21546  isphld  21570  islinds4  21751  lvecisfrlm  21759  cvsi  25037  0nellinds  33348  lindssn  33356  linds2eq  33359  exsslsb  33599  lvecdim0i  33608  lssdimle  33610  tngdim  33616  matdim  33618  lbslsat  33619  lsatdim  33620  drngdimgt0  33621  lindsunlem  33627  lindsun  33628  lbsdiflsp0  33629  dimkerim  33630  qusdimsum  33631  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdg1id  33668  ccfldextdgrr  33674  lindsadd  37614  lshpnelb  38984  lshpnel2N  38985  lshpdisj  38987  lshpcmp  38988  lsatcmp  39003  lsatcmp2  39004  lsatel  39005  lsatelbN  39006  lsatfixedN  39009  lsmcv2  39029  lsatcv0  39031  lsatcveq0  39032  lsat0cv  39033  lcvp  39040  lcv1  39041  lcv2  39042  lsatexch  39043  lsatnem0  39045  lsatexch1  39046  lsatcv0eq  39047  lsatcv1  39048  lsatcvatlem  39049  lsatcvat  39050  lsatcvat2  39051  lsatcvat3  39052  islshpcv  39053  l1cvpat  39054  l1cvat  39055  lfl1  39070  lkrsc  39097  lkrscss  39098  eqlkr  39099  eqlkr3  39101  lkrlsp  39102  lkrlsp3  39104  lkrshp  39105  lkrshp3  39106  lkrshpor  39107  lkrshp4  39108  lshpsmreu  39109  lshpkrlem1  39110  lshpkrlem4  39113  lshpkrlem5  39114  lshpkrlem6  39115  lshpkr  39117  lshpkrex  39118  lfl1dim  39121  lfl1dim2N  39122  lduallvec  39154  lduallkr3  39162  lkrpssN  39163  ldual1dim  39166  lkrss2N  39169  lkreqN  39170  lkrlspeqN  39171  dva0g  41028  dia1dim2  41063  dia1dimid  41064  dia2dimlem5  41069  dia2dimlem7  41071  dia2dimlem9  41073  dia2dimlem10  41074  dia2dimlem13  41077  dvhlmod  41111  diblsmopel  41172  lclkrlem2m  41520  lclkrlem2n  41521  lcfrlem1  41543  lcfrlem2  41544  lcfrlem3  41545  lcdlmod  41593  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdindp0  41720  mapdindp1  41721  mapdindp2  41722  mapdindp3  41723  mapdindp4  41724  lspindp5  41771  lvecgrp  42532  lvecring  42533  prjspersym  42602  prjsper  42603  prjspreln0  42604  prjspvs  42605  prjspeclsp  42607  0prjspn  42623  lincreslvec3  48475  isldepslvec2  48478  lindssnlvec  48479  lvecpsslmod  48500