Theorem lveclmod 21122

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  Scalarcsca 17300  DivRingcdr 20745  LModclmod 20874  LVecclvec 21118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-lvec 21119

This theorem is referenced by:  lveclmodd  21123  lsslvec  21125  lvecvs0or  21127  lssvs0or  21129  lvecvscan  21130  lvecvscan2  21131  lvecinv  21132  lspsnvs  21133  lspsneleq  21134  lspsncmp  21135  lspsnne1  21136  lspsnnecom  21138  lspabs2  21139  lspabs3  21140  lspsneq  21141  ellspsn4  21143  lspdisj  21144  lspdisjb  21145  lspdisj2  21146  lspfixed  21147  lspexch  21148  lspexchn1  21149  lspindpi  21151  lvecindp  21157  lvecindp2  21158  lsmcv  21160  lspsolv  21162  lssacsex  21163  lspsnat  21164  lsppratlem2  21167  lsppratlem3  21168  lsppratlem4  21169  lsppratlem6  21171  lspprat  21172  islbs2  21173  islbs3  21174  lbsacsbs  21175  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  phllmod  21665  isphld  21689  islinds4  21872  lvecisfrlm  21880  cvsi  25176  0nellinds  33377  lindssn  33385  linds2eq  33388  lvecdim0i  33632  lssdimle  33634  tngdim  33640  matdim  33642  lbslsat  33643  lsatdim  33644  drngdimgt0  33645  lindsunlem  33651  lindsun  33652  lbsdiflsp0  33653  dimkerim  33654  qusdimsum  33655  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  extdg1id  33690  ccfldextdgrr  33696  lindsadd  37599  lshpnelb  38965  lshpnel2N  38966  lshpdisj  38968  lshpcmp  38969  lsatcmp  38984  lsatcmp2  38985  lsatel  38986  lsatelbN  38987  lsatfixedN  38990  lsmcv2  39010  lsatcv0  39012  lsatcveq0  39013  lsat0cv  39014  lcvp  39021  lcv1  39022  lcv2  39023  lsatexch  39024  lsatnem0  39026  lsatexch1  39027  lsatcv0eq  39028  lsatcv1  39029  lsatcvatlem  39030  lsatcvat  39031  lsatcvat2  39032  lsatcvat3  39033  islshpcv  39034  l1cvpat  39035  l1cvat  39036  lfl1  39051  lkrsc  39078  lkrscss  39079  eqlkr  39080  eqlkr3  39082  lkrlsp  39083  lkrlsp3  39085  lkrshp  39086  lkrshp3  39087  lkrshpor  39088  lkrshp4  39089  lshpsmreu  39090  lshpkrlem1  39091  lshpkrlem4  39094  lshpkrlem5  39095  lshpkrlem6  39096  lshpkr  39098  lshpkrex  39099  lfl1dim  39102  lfl1dim2N  39103  lduallvec  39135  lduallkr3  39143  lkrpssN  39144  ldual1dim  39147  lkrss2N  39150  lkreqN  39151  lkrlspeqN  39152  dva0g  41009  dia1dim2  41044  dia1dimid  41045  dia2dimlem5  41050  dia2dimlem7  41052  dia2dimlem9  41054  dia2dimlem10  41055  dia2dimlem13  41058  dvhlmod  41092  diblsmopel  41153  lclkrlem2m  41501  lclkrlem2n  41502  lcfrlem1  41524  lcfrlem2  41525  lcfrlem3  41526  lcdlmod  41574  baerlem3lem1  41689  baerlem5alem1  41690  baerlem5blem1  41691  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdindp0  41701  mapdindp1  41702  mapdindp2  41703  mapdindp3  41704  mapdindp4  41705  lspindp5  41752  lvecgrp  42523  lvecring  42524  prjspersym  42593  prjsper  42594  prjspreln0  42595  prjspvs  42596  prjspeclsp  42598  0prjspn  42614  lincreslvec3  48327  isldepslvec2  48330  lindssnlvec  48331  lvecpsslmod  48352