Theorem lveclmod 20377

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  Scalarcsca 16974  DivRingcdr 20000  LModclmod 20132  LVecclvec 20373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-lvec 20374

This theorem is referenced by:  lsslvec  20378  lvecvs0or  20379  lssvs0or  20381  lvecvscan  20382  lvecvscan2  20383  lvecinv  20384  lspsnvs  20385  lspsneleq  20386  lspsncmp  20387  lspsnne1  20388  lspsnnecom  20390  lspabs2  20391  lspabs3  20392  lspsneq  20393  lspsnel4  20395  lspdisj  20396  lspdisjb  20397  lspdisj2  20398  lspfixed  20399  lspexch  20400  lspexchn1  20401  lspindpi  20403  lvecindp  20409  lvecindp2  20410  lsmcv  20412  lspsolv  20414  lssacsex  20415  lspsnat  20416  lsppratlem2  20419  lsppratlem3  20420  lsppratlem4  20421  lsppratlem6  20423  lspprat  20424  islbs2  20425  islbs3  20426  lbsacsbs  20427  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  phllmod  20844  isphld  20868  islinds4  21051  lvecisfrlm  21059  cvsi  24302  0nellinds  31575  lindssn  31582  linds2eq  31584  lvecdim0i  31698  lssdimle  31700  tngdim  31705  matdim  31707  lbslsat  31708  lsatdim  31709  drngdimgt0  31710  lindsunlem  31714  lindsun  31715  lbsdiflsp0  31716  dimkerim  31717  qusdimsum  31718  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  extdg1id  31747  ccfldextdgrr  31751  lindsadd  35779  lshpnelb  37005  lshpnel2N  37006  lshpdisj  37008  lshpcmp  37009  lsatcmp  37024  lsatcmp2  37025  lsatel  37026  lsatelbN  37027  lsatfixedN  37030  lsmcv2  37050  lsatcv0  37052  lsatcveq0  37053  lsat0cv  37054  lcvp  37061  lcv1  37062  lcv2  37063  lsatexch  37064  lsatnem0  37066  lsatexch1  37067  lsatcv0eq  37068  lsatcv1  37069  lsatcvatlem  37070  lsatcvat  37071  lsatcvat2  37072  lsatcvat3  37073  islshpcv  37074  l1cvpat  37075  l1cvat  37076  lfl1  37091  lkrsc  37118  lkrscss  37119  eqlkr  37120  eqlkr3  37122  lkrlsp  37123  lkrlsp3  37125  lkrshp  37126  lkrshp3  37127  lkrshpor  37128  lkrshp4  37129  lshpsmreu  37130  lshpkrlem1  37131  lshpkrlem4  37134  lshpkrlem5  37135  lshpkrlem6  37136  lshpkr  37138  lshpkrex  37139  lfl1dim  37142  lfl1dim2N  37143  lduallvec  37175  lduallkr3  37183  lkrpssN  37184  ldual1dim  37187  lkrss2N  37190  lkreqN  37191  lkrlspeqN  37192  dva0g  39048  dia1dim2  39083  dia1dimid  39084  dia2dimlem5  39089  dia2dimlem7  39091  dia2dimlem9  39093  dia2dimlem10  39094  dia2dimlem13  39097  dvhlmod  39131  diblsmopel  39192  lclkrlem2m  39540  lclkrlem2n  39541  lcfrlem1  39563  lcfrlem2  39564  lcfrlem3  39565  lcdlmod  39613  baerlem3lem1  39728  baerlem5alem1  39729  baerlem5blem1  39730  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  baerlem5amN  39737  baerlem5bmN  39738  baerlem5abmN  39739  mapdindp0  39740  mapdindp1  39741  mapdindp2  39742  mapdindp3  39743  mapdindp4  39744  lspindp5  39791  lvecgrp  40264  lveclmodd  40265  lvecring  40267  prjspersym  40453  prjsper  40454  prjspreln0  40455  prjspvs  40456  prjspeclsp  40458  0prjspn  40472  lincreslvec3  45834  isldepslvec2  45837  lindssnlvec  45838  lvecpsslmod  45859