Theorem lveclmod 21105

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6561  Scalarcsca 17300  DivRingcdr 20729  LModclmod 20858  LVecclvec 21101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-lvec 21102

This theorem is referenced by:  lveclmodd  21106  lsslvec  21108  lvecvs0or  21110  lssvs0or  21112  lvecvscan  21113  lvecvscan2  21114  lvecinv  21115  lspsnvs  21116  lspsneleq  21117  lspsncmp  21118  lspsnne1  21119  lspsnnecom  21121  lspabs2  21122  lspabs3  21123  lspsneq  21124  ellspsn4  21126  lspdisj  21127  lspdisjb  21128  lspdisj2  21129  lspfixed  21130  lspexch  21131  lspexchn1  21132  lspindpi  21134  lvecindp  21140  lvecindp2  21141  lsmcv  21143  lspsolv  21145  lssacsex  21146  lspsnat  21147  lsppratlem2  21150  lsppratlem3  21151  lsppratlem4  21152  lsppratlem6  21154  lspprat  21155  islbs2  21156  islbs3  21157  lbsacsbs  21158  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  phllmod  21648  isphld  21672  islinds4  21855  lvecisfrlm  21863  cvsi  25163  0nellinds  33398  lindssn  33406  linds2eq  33409  exsslsb  33647  lvecdim0i  33656  lssdimle  33658  tngdim  33664  matdim  33666  lbslsat  33667  lsatdim  33668  drngdimgt0  33669  lindsunlem  33675  lindsun  33676  lbsdiflsp0  33677  dimkerim  33678  qusdimsum  33679  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  extdg1id  33716  ccfldextdgrr  33722  lindsadd  37620  lshpnelb  38985  lshpnel2N  38986  lshpdisj  38988  lshpcmp  38989  lsatcmp  39004  lsatcmp2  39005  lsatel  39006  lsatelbN  39007  lsatfixedN  39010  lsmcv2  39030  lsatcv0  39032  lsatcveq0  39033  lsat0cv  39034  lcvp  39041  lcv1  39042  lcv2  39043  lsatexch  39044  lsatnem0  39046  lsatexch1  39047  lsatcv0eq  39048  lsatcv1  39049  lsatcvatlem  39050  lsatcvat  39051  lsatcvat2  39052  lsatcvat3  39053  islshpcv  39054  l1cvpat  39055  l1cvat  39056  lfl1  39071  lkrsc  39098  lkrscss  39099  eqlkr  39100  eqlkr3  39102  lkrlsp  39103  lkrlsp3  39105  lkrshp  39106  lkrshp3  39107  lkrshpor  39108  lkrshp4  39109  lshpsmreu  39110  lshpkrlem1  39111  lshpkrlem4  39114  lshpkrlem5  39115  lshpkrlem6  39116  lshpkr  39118  lshpkrex  39119  lfl1dim  39122  lfl1dim2N  39123  lduallvec  39155  lduallkr3  39163  lkrpssN  39164  ldual1dim  39167  lkrss2N  39170  lkreqN  39171  lkrlspeqN  39172  dva0g  41029  dia1dim2  41064  dia1dimid  41065  dia2dimlem5  41070  dia2dimlem7  41072  dia2dimlem9  41074  dia2dimlem10  41075  dia2dimlem13  41078  dvhlmod  41112  diblsmopel  41173  lclkrlem2m  41521  lclkrlem2n  41522  lcfrlem1  41544  lcfrlem2  41545  lcfrlem3  41546  lcdlmod  41594  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdindp0  41721  mapdindp1  41722  mapdindp2  41723  mapdindp3  41724  mapdindp4  41725  lspindp5  41772  lvecgrp  42547  lvecring  42548  prjspersym  42617  prjsper  42618  prjspreln0  42619  prjspvs  42620  prjspeclsp  42622  0prjspn  42638  lincreslvec3  48399  isldepslvec2  48402  lindssnlvec  48403  lvecpsslmod  48424