Theorem lveclmod 21128

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  Scalarcsca 17314  DivRingcdr 20751  LModclmod 20880  LVecclvec 21124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-lvec 21125

This theorem is referenced by:  lveclmodd  21129  lsslvec  21131  lvecvs0or  21133  lssvs0or  21135  lvecvscan  21136  lvecvscan2  21137  lvecinv  21138  lspsnvs  21139  lspsneleq  21140  lspsncmp  21141  lspsnne1  21142  lspsnnecom  21144  lspabs2  21145  lspabs3  21146  lspsneq  21147  ellspsn4  21149  lspdisj  21150  lspdisjb  21151  lspdisj2  21152  lspfixed  21153  lspexch  21154  lspexchn1  21155  lspindpi  21157  lvecindp  21163  lvecindp2  21164  lsmcv  21166  lspsolv  21168  lssacsex  21169  lspsnat  21170  lsppratlem2  21173  lsppratlem3  21174  lsppratlem4  21175  lsppratlem6  21177  lspprat  21178  islbs2  21179  islbs3  21180  lbsacsbs  21181  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  phllmod  21671  isphld  21695  islinds4  21878  lvecisfrlm  21886  cvsi  25182  0nellinds  33363  lindssn  33371  linds2eq  33374  lvecdim0i  33618  lssdimle  33620  tngdim  33626  matdim  33628  lbslsat  33629  lsatdim  33630  drngdimgt0  33631  lindsunlem  33637  lindsun  33638  lbsdiflsp0  33639  dimkerim  33640  qusdimsum  33641  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33676  ccfldextdgrr  33682  lindsadd  37573  lshpnelb  38940  lshpnel2N  38941  lshpdisj  38943  lshpcmp  38944  lsatcmp  38959  lsatcmp2  38960  lsatel  38961  lsatelbN  38962  lsatfixedN  38965  lsmcv2  38985  lsatcv0  38987  lsatcveq0  38988  lsat0cv  38989  lcvp  38996  lcv1  38997  lcv2  38998  lsatexch  38999  lsatnem0  39001  lsatexch1  39002  lsatcv0eq  39003  lsatcv1  39004  lsatcvatlem  39005  lsatcvat  39006  lsatcvat2  39007  lsatcvat3  39008  islshpcv  39009  l1cvpat  39010  l1cvat  39011  lfl1  39026  lkrsc  39053  lkrscss  39054  eqlkr  39055  eqlkr3  39057  lkrlsp  39058  lkrlsp3  39060  lkrshp  39061  lkrshp3  39062  lkrshpor  39063  lkrshp4  39064  lshpsmreu  39065  lshpkrlem1  39066  lshpkrlem4  39069  lshpkrlem5  39070  lshpkrlem6  39071  lshpkr  39073  lshpkrex  39074  lfl1dim  39077  lfl1dim2N  39078  lduallvec  39110  lduallkr3  39118  lkrpssN  39119  ldual1dim  39122  lkrss2N  39125  lkreqN  39126  lkrlspeqN  39127  dva0g  40984  dia1dim2  41019  dia1dimid  41020  dia2dimlem5  41025  dia2dimlem7  41027  dia2dimlem9  41029  dia2dimlem10  41030  dia2dimlem13  41033  dvhlmod  41067  diblsmopel  41128  lclkrlem2m  41476  lclkrlem2n  41477  lcfrlem1  41499  lcfrlem2  41500  lcfrlem3  41501  lcdlmod  41549  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdindp0  41676  mapdindp1  41677  mapdindp2  41678  mapdindp3  41679  mapdindp4  41680  lspindp5  41727  lvecgrp  42492  lvecring  42493  prjspersym  42562  prjsper  42563  prjspreln0  42564  prjspvs  42565  prjspeclsp  42567  0prjspn  42583  lincreslvec3  48211  isldepslvec2  48214  lindssnlvec  48215  lvecpsslmod  48236