Theorem lveclmod 21070

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6500  Scalarcsca 17192  DivRingcdr 20674  LModclmod 20823  LVecclvec 21066

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-lvec 21067

This theorem is referenced by:  lveclmodd  21071  lsslvec  21073  lvecvs0or  21075  lssvs0or  21077  lvecvscan  21078  lvecvscan2  21079  lvecinv  21080  lspsnvs  21081  lspsneleq  21082  lspsncmp  21083  lspsnne1  21084  lspsnnecom  21086  lspabs2  21087  lspabs3  21088  lspsneq  21089  ellspsn4  21091  lspdisj  21092  lspdisjb  21093  lspdisj2  21094  lspfixed  21095  lspexch  21096  lspexchn1  21097  lspindpi  21099  lvecindp  21105  lvecindp2  21106  lsmcv  21108  lspsolv  21110  lssacsex  21111  lspsnat  21112  lsppratlem2  21115  lsppratlem3  21116  lsppratlem4  21117  lsppratlem6  21119  lspprat  21120  islbs2  21121  islbs3  21122  lbsacsbs  21123  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  phllmod  21597  isphld  21621  islinds4  21802  lvecisfrlm  21810  cvsi  25098  0nellinds  33462  lindssn  33470  linds2eq  33473  exsslsb  33773  lvecdim0i  33782  lssdimle  33784  tngdim  33790  matdim  33792  lbslsat  33793  lsatdim  33794  drngdimgt0  33795  lindsunlem  33801  lindsun  33802  lbsdiflsp0  33803  dimkerim  33804  qusdimsum  33805  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  extdg1id  33843  ccfldextdgrr  33849  lindsadd  37853  lshpnelb  39349  lshpnel2N  39350  lshpdisj  39352  lshpcmp  39353  lsatcmp  39368  lsatcmp2  39369  lsatel  39370  lsatelbN  39371  lsatfixedN  39374  lsmcv2  39394  lsatcv0  39396  lsatcveq0  39397  lsat0cv  39398  lcvp  39405  lcv1  39406  lcv2  39407  lsatexch  39408  lsatnem0  39410  lsatexch1  39411  lsatcv0eq  39412  lsatcv1  39413  lsatcvatlem  39414  lsatcvat  39415  lsatcvat2  39416  lsatcvat3  39417  islshpcv  39418  l1cvpat  39419  l1cvat  39420  lfl1  39435  lkrsc  39462  lkrscss  39463  eqlkr  39464  eqlkr3  39466  lkrlsp  39467  lkrlsp3  39469  lkrshp  39470  lkrshp3  39471  lkrshpor  39472  lkrshp4  39473  lshpsmreu  39474  lshpkrlem1  39475  lshpkrlem4  39478  lshpkrlem5  39479  lshpkrlem6  39480  lshpkr  39482  lshpkrex  39483  lfl1dim  39486  lfl1dim2N  39487  lduallvec  39519  lduallkr3  39527  lkrpssN  39528  ldual1dim  39531  lkrss2N  39534  lkreqN  39535  lkrlspeqN  39536  dva0g  41392  dia1dim2  41427  dia1dimid  41428  dia2dimlem5  41433  dia2dimlem7  41435  dia2dimlem9  41437  dia2dimlem10  41438  dia2dimlem13  41441  dvhlmod  41475  diblsmopel  41536  lclkrlem2m  41884  lclkrlem2n  41885  lcfrlem1  41907  lcfrlem2  41908  lcfrlem3  41909  lcdlmod  41957  baerlem3lem1  42072  baerlem5alem1  42073  baerlem5blem1  42074  baerlem3lem2  42075  baerlem5alem2  42076  baerlem5blem2  42077  baerlem5amN  42081  baerlem5bmN  42082  baerlem5abmN  42083  mapdindp0  42084  mapdindp1  42085  mapdindp2  42086  mapdindp3  42087  mapdindp4  42088  lspindp5  42135  lvecgrp  42896  lvecring  42897  prjspersym  42954  prjsper  42955  prjspreln0  42956  prjspvs  42957  prjspeclsp  42959  0prjspn  42975  lincreslvec3  48831  isldepslvec2  48834  lindssnlvec  48835  lvecpsslmod  48856