Theorem lveclmod 19465

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

Syntax hints:   → wi 4   ∈ wcel 2164  ‘cfv 6123  Scalarcsca 16308  DivRingcdr 19103  LModclmod 19219  LVecclvec 19461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-lvec 19462

This theorem is referenced by:  lsslvec  19466  lvecvs0or  19467  lssvs0or  19469  lvecvscan  19470  lvecvscan2  19471  lvecinv  19472  lspsnvs  19473  lspsneleq  19474  lspsncmp  19475  lspsnne1  19476  lspsnnecom  19478  lspabs2  19479  lspabs3  19480  lspsneq  19481  lspsnel4  19483  lspdisj  19484  lspdisjb  19485  lspdisj2  19486  lspfixed  19487  lspfixedOLD  19488  lspexch  19489  lspexchn1  19490  lspindpi  19492  lvecindp  19498  lvecindp2  19499  lsmcv  19501  lspsolv  19503  lssacsex  19504  lspsnat  19505  lsppratlem2  19509  lsppratlem3  19510  lsppratlem4  19511  lsppratlem6  19513  lspprat  19514  islbs2  19515  islbs3  19516  lbsacsbs  19517  lbsextlem2  19520  lbsextlem3  19521  lbsextlem4  19522  phllmod  20337  isphld  20361  islinds4  20541  lvecisfrlm  20549  cvsi  23299  lindsadd  33939  lshpnelb  35052  lshpnel2N  35053  lshpdisj  35055  lshpcmp  35056  lsatcmp  35071  lsatcmp2  35072  lsatel  35073  lsatelbN  35074  lsatfixedN  35077  lsmcv2  35097  lsatcv0  35099  lsatcveq0  35100  lsat0cv  35101  lcvp  35108  lcv1  35109  lcv2  35110  lsatexch  35111  lsatnem0  35113  lsatexch1  35114  lsatcv0eq  35115  lsatcv1  35116  lsatcvatlem  35117  lsatcvat  35118  lsatcvat2  35119  lsatcvat3  35120  islshpcv  35121  l1cvpat  35122  l1cvat  35123  lfl1  35138  lkrsc  35165  lkrscss  35166  eqlkr  35167  eqlkr3  35169  lkrlsp  35170  lkrlsp3  35172  lkrshp  35173  lkrshp3  35174  lkrshpor  35175  lkrshp4  35176  lshpsmreu  35177  lshpkrlem1  35178  lshpkrlem4  35181  lshpkrlem5  35182  lshpkrlem6  35183  lshpkr  35185  lshpkrex  35186  lfl1dim  35189  lfl1dim2N  35190  lduallvec  35222  lduallkr3  35230  lkrpssN  35231  ldual1dim  35234  lkrss2N  35237  lkreqN  35238  lkrlspeqN  35239  dva0g  37095  dia1dim2  37130  dia1dimid  37131  dia2dimlem5  37136  dia2dimlem7  37138  dia2dimlem9  37140  dia2dimlem10  37141  dia2dimlem13  37144  dvhlmod  37178  diblsmopel  37239  lclkrlem2m  37587  lclkrlem2n  37588  lcfrlem1  37610  lcfrlem2  37611  lcfrlem3  37612  lcdlmod  37660  baerlem3lem1  37775  baerlem5alem1  37776  baerlem5blem1  37777  baerlem3lem2  37778  baerlem5alem2  37779  baerlem5blem2  37780  baerlem5amN  37784  baerlem5bmN  37785  baerlem5abmN  37786  mapdindp0  37787  mapdindp1  37788  mapdindp2  37789  mapdindp3  37790  mapdindp4  37791  lspindp5  37838  lincreslvec3  43111  isldepslvec2  43114  lindssnlvec  43115  lvecpsslmod  43136