Theorem lveclmod 20705

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6540  Scalarcsca 17196  DivRingcdr 20304  LModclmod 20459  LVecclvec 20701

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-lvec 20702

This theorem is referenced by:  lveclmodd  20706  lsslvec  20707  lvecvs0or  20709  lssvs0or  20711  lvecvscan  20712  lvecvscan2  20713  lvecinv  20714  lspsnvs  20715  lspsneleq  20716  lspsncmp  20717  lspsnne1  20718  lspsnnecom  20720  lspabs2  20721  lspabs3  20722  lspsneq  20723  lspsnel4  20725  lspdisj  20726  lspdisjb  20727  lspdisj2  20728  lspfixed  20729  lspexch  20730  lspexchn1  20731  lspindpi  20733  lvecindp  20739  lvecindp2  20740  lsmcv  20742  lspsolv  20744  lssacsex  20745  lspsnat  20746  lsppratlem2  20749  lsppratlem3  20750  lsppratlem4  20751  lsppratlem6  20753  lspprat  20754  islbs2  20755  islbs3  20756  lbsacsbs  20757  lbsextlem2  20760  lbsextlem3  20761  lbsextlem4  20762  phllmod  21167  isphld  21191  islinds4  21374  lvecisfrlm  21382  cvsi  24628  0nellinds  32452  lindssn  32459  linds2eq  32462  lvecdim0i  32636  lssdimle  32638  tngdim  32643  matdim  32645  lbslsat  32646  lsatdim  32647  drngdimgt0  32648  lindsunlem  32654  lindsun  32655  lbsdiflsp0  32656  dimkerim  32657  qusdimsum  32658  fedgmullem1  32659  fedgmullem2  32660  fedgmul  32661  extdg1id  32687  ccfldextdgrr  32691  lindsadd  36419  lshpnelb  37792  lshpnel2N  37793  lshpdisj  37795  lshpcmp  37796  lsatcmp  37811  lsatcmp2  37812  lsatel  37813  lsatelbN  37814  lsatfixedN  37817  lsmcv2  37837  lsatcv0  37839  lsatcveq0  37840  lsat0cv  37841  lcvp  37848  lcv1  37849  lcv2  37850  lsatexch  37851  lsatnem0  37853  lsatexch1  37854  lsatcv0eq  37855  lsatcv1  37856  lsatcvatlem  37857  lsatcvat  37858  lsatcvat2  37859  lsatcvat3  37860  islshpcv  37861  l1cvpat  37862  l1cvat  37863  lfl1  37878  lkrsc  37905  lkrscss  37906  eqlkr  37907  eqlkr3  37909  lkrlsp  37910  lkrlsp3  37912  lkrshp  37913  lkrshp3  37914  lkrshpor  37915  lkrshp4  37916  lshpsmreu  37917  lshpkrlem1  37918  lshpkrlem4  37921  lshpkrlem5  37922  lshpkrlem6  37923  lshpkr  37925  lshpkrex  37926  lfl1dim  37929  lfl1dim2N  37930  lduallvec  37962  lduallkr3  37970  lkrpssN  37971  ldual1dim  37974  lkrss2N  37977  lkreqN  37978  lkrlspeqN  37979  dva0g  39836  dia1dim2  39871  dia1dimid  39872  dia2dimlem5  39877  dia2dimlem7  39879  dia2dimlem9  39881  dia2dimlem10  39882  dia2dimlem13  39885  dvhlmod  39919  diblsmopel  39980  lclkrlem2m  40328  lclkrlem2n  40329  lcfrlem1  40351  lcfrlem2  40352  lcfrlem3  40353  lcdlmod  40401  baerlem3lem1  40516  baerlem5alem1  40517  baerlem5blem1  40518  baerlem3lem2  40519  baerlem5alem2  40520  baerlem5blem2  40521  baerlem5amN  40525  baerlem5bmN  40526  baerlem5abmN  40527  mapdindp0  40528  mapdindp1  40529  mapdindp2  40530  mapdindp3  40531  mapdindp4  40532  lspindp5  40579  lvecgrp  41056  lvecring  41058  prjspersym  41293  prjsper  41294  prjspreln0  41295  prjspvs  41296  prjspeclsp  41298  0prjspn  41314  lincreslvec3  47065  isldepslvec2  47068  lindssnlvec  47069  lvecpsslmod  47090