Theorem lveclmod 21411

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6558  Scalarcsca 17460  DivRingcdr 21010  LModclmod 21165  LVecclvec 21407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-lvec 21408

This theorem is used by:  lveclmodd  21412  lsslvec  21414  lvecvs0or  21416  lssvs0or  21418  lvecvscan  21419  lvecvscan2  21420  lvecinv  21421  lspsnvs  21422  lspsneleq  21423  lspsncmp  21424  lspsnne1  21425  lspsnnecom  21427  lspabs2  21428  lspabs3  21429  lspsneq  21430  ellspsn4  21432  lspdisj  21433  lspdisjb  21434  lspdisj2  21435  lspfixed  21436  lspexch  21437  lspexchn1  21438  lspindpi  21440  lvecindp  21446  lvecindp2  21447  lsmcv  21449  lspsolv  21451  lssacsex  21452  lspsnat  21453  lsppratlem2  21456  lsppratlem3  21457  lsppratlem4  21458  lsppratlem6  21460  lspprat  21461  islbs2  21462  islbs3  21463  lbsacsbs  21464  lbsextlem2  21467  lbsextlem3  21468  lbsextlem4  21469  phllmod  21966  isphld  21990  islinds4  22171  lvecisfrlm  22179  cvsi  25481  0nellinds  33996  lindssn  34003  linds2eq  34006  exsslsb  34299  lvecdim0i  34308  lssdimle  34310  tngdim  34315  matdim  34317  lbslsat  34318  lsatdim  34319  drngdimgt0  34320  lindsunlem  34326  lindsun  34327  lbsdiflsp0  34328  dimkerim  34329  qusdimsum  34330  fedgmullem1  34331  fedgmullem2  34332  extdg1id  34368  ccfldextdgrr  34374  lindsadd  38728  lshpnelb  40233  lshpnel2N  40234  lshpdisj  40236  lshpcmp  40237  lsatcmp  40252  lsatcmp2  40253  lsatel  40254  lsatelbN  40255  lsatfixedN  40258  lsmcv2  40278  lsatcv0  40280  lsatcveq0  40281  lsat0cv  40282  lcvp  40289  lcv1  40290  lcv2  40291  lsatexch  40292  lsatnem0  40294  lsatexch1  40295  lsatcv0eq  40296  lsatcv1  40297  lsatcvatlem  40298  lsatcvat  40299  lsatcvat2  40300  lsatcvat3  40301  islshpcv  40302  l1cvpat  40303  l1cvat  40304  lfl1  40319  lkrsc  40346  lkrscss  40347  eqlkr  40348  eqlkr3  40350  lkrlsp  40351  lkrlsp3  40353  lkrshp  40354  lkrshp3  40355  lkrshpor  40356  lkrshp4  40357  lshpsmreu  40358  lshpkrlem1  40359  lshpkrlem4  40362  lshpkrlem5  40363  lshpkrlem6  40364  lshpkr  40366  lshpkrex  40367  lfl1dim  40370  lfl1dim2N  40371  lduallvec  40403  lduallkr3  40411  lkrpssN  40412  ldual1dim  40415  lkrss2N  40418  lkreqN  40419  lkrlspeqN  40420  dva0g  42276  dia1dim2  42311  dia1dimid  42312  dia2dimlem5  42317  dia2dimlem7  42319  dia2dimlem9  42321  dia2dimlem10  42322  dia2dimlem13  42325  dvhlmod  42359  diblsmopel  42420  lclkrlem2m  42768  lclkrlem2n  42769  lcfrlem1  42791  lcfrlem2  42792  lcfrlem3  42793  lcdlmod  42841  baerlem3lem1  42956  baerlem5alem1  42957  baerlem5blem1  42958  baerlem3lem2  42959  baerlem5alem2  42960  baerlem5blem2  42961  baerlem5amN  42965  baerlem5bmN  42966  baerlem5abmN  42967  mapdindp0  42968  mapdindp1  42969  mapdindp2  42970  mapdindp3  42971  mapdindp4  42972  lspindp5  43019  lvecgrp  43794  lvecring  43795  prjspersym  43828  prjsper  43829  prjspreln0  43830  prjspvs  43831  prjspeclsp  43833  lincreslvec3  49799  isldepslvec2  49802  lindssnlvec  49803  lvecpsslmod  49824