Theorem lveclmod 18927

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

Syntax hints:   → wi 4   ∈ wcel 1977  ‘cfv 5804  Scalarcsca 15771  DivRingcdr 18570  LModclmod 18686  LVecclvec 18923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-lvec 18924

This theorem is referenced by:  lsslvec  18928  lvecvs0or  18929  lssvs0or  18931  lvecvscan  18932  lvecvscan2  18933  lvecinv  18934  lspsnvs  18935  lspsneleq  18936  lspsncmp  18937  lspsnne1  18938  lspsnnecom  18940  lspabs2  18941  lspabs3  18942  lspsneq  18943  lspsnel4  18945  lspdisj  18946  lspdisjb  18947  lspdisj2  18948  lspfixed  18949  lspexch  18950  lspexchn1  18951  lspindpi  18953  lvecindp  18959  lvecindp2  18960  lsmcv  18962  lspsolv  18964  lssacsex  18965  lspsnat  18966  lsppratlem2  18969  lsppratlem3  18970  lsppratlem4  18971  lsppratlem6  18973  lspprat  18974  islbs2  18975  islbs3  18976  lbsacsbs  18977  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  phllmod  19794  isphld  19818  islinds4  19993  lvecisfrlm  20001  cvsi  22738  lshpnelb  33289  lshpnel2N  33290  lshpdisj  33292  lshpcmp  33293  lsatcmp  33308  lsatcmp2  33309  lsatel  33310  lsatelbN  33311  lsatfixedN  33314  lsmcv2  33334  lsatcv0  33336  lsatcveq0  33337  lsat0cv  33338  lcvp  33345  lcv1  33346  lcv2  33347  lsatexch  33348  lsatnem0  33350  lsatexch1  33351  lsatcv0eq  33352  lsatcv1  33353  lsatcvatlem  33354  lsatcvat  33355  lsatcvat2  33356  lsatcvat3  33357  islshpcv  33358  l1cvpat  33359  l1cvat  33360  lfl1  33375  lkrsc  33402  lkrscss  33403  eqlkr  33404  eqlkr3  33406  lkrlsp  33407  lkrlsp3  33409  lkrshp  33410  lkrshp3  33411  lkrshpor  33412  lkrshp4  33413  lshpsmreu  33414  lshpkrlem1  33415  lshpkrlem4  33418  lshpkrlem5  33419  lshpkrlem6  33420  lshpkr  33422  lshpkrex  33423  lfl1dim  33426  lfl1dim2N  33427  lduallvec  33459  lduallkr3  33467  lkrpssN  33468  ldual1dim  33471  lkrss2N  33474  lkreqN  33475  lkrlspeqN  33476  dva0g  35334  dia1dim2  35369  dia1dimid  35370  dia2dimlem5  35375  dia2dimlem7  35377  dia2dimlem9  35379  dia2dimlem10  35380  dia2dimlem13  35383  dvhlmod  35417  diblsmopel  35478  lclkrlem2m  35826  lclkrlem2n  35827  lcfrlem1  35849  lcfrlem2  35850  lcfrlem3  35851  lcdlmod  35899  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp0  36026  mapdindp1  36027  mapdindp2  36028  mapdindp3  36029  mapdindp4  36030  lspindp5  36077  lincreslvec3  42065  isldepslvec2  42068  lindssnlvec  42069  lvecpsslmod  42090