Theorem lveclmod 21343

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6527  Scalarcsca 17393  DivRingcdr 20942  LModclmod 21097  LVecclvec 21339

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-lvec 21340

This theorem is used by:  lveclmodd  21344  lsslvec  21346  lvecvs0or  21348  lssvs0or  21350  lvecvscan  21351  lvecvscan2  21352  lvecinv  21353  lspsnvs  21354  lspsneleq  21355  lspsncmp  21356  lspsnne1  21357  lspsnnecom  21359  lspabs2  21360  lspabs3  21361  lspsneq  21362  ellspsn4  21364  lspdisj  21365  lspdisjb  21366  lspdisj2  21367  lspfixed  21368  lspexch  21369  lspexchn1  21370  lspindpi  21372  lvecindp  21378  lvecindp2  21379  lsmcv  21381  lspsolv  21383  lssacsex  21384  lspsnat  21385  lsppratlem2  21388  lsppratlem3  21389  lsppratlem4  21390  lsppratlem6  21392  lspprat  21393  islbs2  21394  islbs3  21395  lbsacsbs  21396  lbsextlem2  21399  lbsextlem3  21400  lbsextlem4  21401  phllmod  21898  isphld  21922  islinds4  22103  lvecisfrlm  22111  cvsi  25413  0nellinds  33860  lindssn  33867  linds2eq  33870  exsslsb  34163  lvecdim0i  34172  lssdimle  34174  tngdim  34179  matdim  34181  lbslsat  34182  lsatdim  34183  drngdimgt0  34184  lindsunlem  34190  lindsun  34191  lbsdiflsp0  34192  dimkerim  34193  qusdimsum  34194  fedgmullem1  34195  fedgmullem2  34196  fedgmul  34197  extdg1id  34232  ccfldextdgrr  34238  lindsadd  38456  lshpnelb  39961  lshpnel2N  39962  lshpdisj  39964  lshpcmp  39965  lsatcmp  39980  lsatcmp2  39981  lsatel  39982  lsatelbN  39983  lsatfixedN  39986  lsmcv2  40006  lsatcv0  40008  lsatcveq0  40009  lsat0cv  40010  lcvp  40017  lcv1  40018  lcv2  40019  lsatexch  40020  lsatnem0  40022  lsatexch1  40023  lsatcv0eq  40024  lsatcv1  40025  lsatcvatlem  40026  lsatcvat  40027  lsatcvat2  40028  lsatcvat3  40029  islshpcv  40030  l1cvpat  40031  l1cvat  40032  lfl1  40047  lkrsc  40074  lkrscss  40075  eqlkr  40076  eqlkr3  40078  lkrlsp  40079  lkrlsp3  40081  lkrshp  40082  lkrshp3  40083  lkrshpor  40084  lkrshp4  40085  lshpsmreu  40086  lshpkrlem1  40087  lshpkrlem4  40090  lshpkrlem5  40091  lshpkrlem6  40092  lshpkr  40094  lshpkrex  40095  lfl1dim  40098  lfl1dim2N  40099  lduallvec  40131  lduallkr3  40139  lkrpssN  40140  ldual1dim  40143  lkrss2N  40146  lkreqN  40147  lkrlspeqN  40148  dva0g  42004  dia1dim2  42039  dia1dimid  42040  dia2dimlem5  42045  dia2dimlem7  42047  dia2dimlem9  42049  dia2dimlem10  42050  dia2dimlem13  42053  dvhlmod  42087  diblsmopel  42148  lclkrlem2m  42496  lclkrlem2n  42497  lcfrlem1  42519  lcfrlem2  42520  lcfrlem3  42521  lcdlmod  42569  baerlem3lem1  42684  baerlem5alem1  42685  baerlem5blem1  42686  baerlem3lem2  42687  baerlem5alem2  42688  baerlem5blem2  42689  baerlem5amN  42693  baerlem5bmN  42694  baerlem5abmN  42695  mapdindp0  42696  mapdindp1  42697  mapdindp2  42698  mapdindp3  42699  mapdindp4  42700  lspindp5  42747  lvecgrp  43523  lvecring  43524  prjspersym  43557  prjsper  43558  prjspreln0  43559  prjspvs  43560  prjspeclsp  43562  0prjspn  43578  lincreslvec3  49516  isldepslvec2  49519  lindssnlvec  49520  lvecpsslmod  49541