Theorem lveclmod 21294

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  Scalarcsca 17349  DivRingcdr 20894  LModclmod 21048  LVecclvec 21290

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-lvec 21291

This theorem is used by:  lveclmodd  21295  lsslvec  21297  lvecvs0or  21299  lssvs0or  21301  lvecvscan  21302  lvecvscan2  21303  lvecinv  21304  lspsnvs  21305  lspsneleq  21306  lspsncmp  21307  lspsnne1  21308  lspsnnecom  21310  lspabs2  21311  lspabs3  21312  lspsneq  21313  ellspsn4  21315  lspdisj  21316  lspdisjb  21317  lspdisj2  21318  lspfixed  21319  lspexch  21320  lspexchn1  21321  lspindpi  21323  lvecindp  21329  lvecindp2  21330  lsmcv  21332  lspsolv  21334  lssacsex  21335  lspsnat  21336  lsppratlem2  21339  lsppratlem3  21340  lsppratlem4  21341  lsppratlem6  21343  lspprat  21344  islbs2  21345  islbs3  21346  lbsacsbs  21347  lbsextlem2  21350  lbsextlem3  21351  lbsextlem4  21352  phllmod  21847  isphld  21871  islinds4  22052  lvecisfrlm  22060  cvsi  25362  0nellinds  33807  lindssn  33813  linds2eq  33816  exsslsb  34109  lvecdim0i  34118  lssdimle  34120  tngdim  34125  matdim  34127  lbslsat  34128  lsatdim  34129  drngdimgt0  34130  lindsunlem  34136  lindsun  34137  lbsdiflsp0  34138  dimkerim  34139  qusdimsum  34140  fedgmullem1  34141  fedgmullem2  34142  fedgmul  34143  extdg1id  34178  ccfldextdgrr  34184  lindsadd  38369  lshpnelb  39859  lshpnel2N  39860  lshpdisj  39862  lshpcmp  39863  lsatcmp  39878  lsatcmp2  39879  lsatel  39880  lsatelbN  39881  lsatfixedN  39884  lsmcv2  39904  lsatcv0  39906  lsatcveq0  39907  lsat0cv  39908  lcvp  39915  lcv1  39916  lcv2  39917  lsatexch  39918  lsatnem0  39920  lsatexch1  39921  lsatcv0eq  39922  lsatcv1  39923  lsatcvatlem  39924  lsatcvat  39925  lsatcvat2  39926  lsatcvat3  39927  islshpcv  39928  l1cvpat  39929  l1cvat  39930  lfl1  39945  lkrsc  39972  lkrscss  39973  eqlkr  39974  eqlkr3  39976  lkrlsp  39977  lkrlsp3  39979  lkrshp  39980  lkrshp3  39981  lkrshpor  39982  lkrshp4  39983  lshpsmreu  39984  lshpkrlem1  39985  lshpkrlem4  39988  lshpkrlem5  39989  lshpkrlem6  39990  lshpkr  39992  lshpkrex  39993  lfl1dim  39996  lfl1dim2N  39997  lduallvec  40029  lduallkr3  40037  lkrpssN  40038  ldual1dim  40041  lkrss2N  40044  lkreqN  40045  lkrlspeqN  40046  dva0g  41902  dia1dim2  41937  dia1dimid  41938  dia2dimlem5  41943  dia2dimlem7  41945  dia2dimlem9  41947  dia2dimlem10  41948  dia2dimlem13  41951  dvhlmod  41985  diblsmopel  42046  lclkrlem2m  42394  lclkrlem2n  42395  lcfrlem1  42417  lcfrlem2  42418  lcfrlem3  42419  lcdlmod  42467  baerlem3lem1  42582  baerlem5alem1  42583  baerlem5blem1  42584  baerlem3lem2  42585  baerlem5alem2  42586  baerlem5blem2  42587  baerlem5amN  42591  baerlem5bmN  42592  baerlem5abmN  42593  mapdindp0  42594  mapdindp1  42595  mapdindp2  42596  mapdindp3  42597  mapdindp4  42598  lspindp5  42645  lvecgrp  43421  lvecring  43422  prjspersym  43455  prjsper  43456  prjspreln0  43457  prjspvs  43458  prjspeclsp  43460  0prjspn  43476  lincreslvec3  49414  isldepslvec2  49417  lindssnlvec  49418  lvecpsslmod  49439