Theorem lveclmod 19872

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

Syntax hints:   → wi 4   ∈ wcel 2110  ‘cfv 6350  Scalarcsca 16562  DivRingcdr 19496  LModclmod 19628  LVecclvec 19868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-lvec 19869

This theorem is referenced by:  lsslvec  19873  lvecvs0or  19874  lssvs0or  19876  lvecvscan  19877  lvecvscan2  19878  lvecinv  19879  lspsnvs  19880  lspsneleq  19881  lspsncmp  19882  lspsnne1  19883  lspsnnecom  19885  lspabs2  19886  lspabs3  19887  lspsneq  19888  lspsnel4  19890  lspdisj  19891  lspdisjb  19892  lspdisj2  19893  lspfixed  19894  lspexch  19895  lspexchn1  19896  lspindpi  19898  lvecindp  19904  lvecindp2  19905  lsmcv  19907  lspsolv  19909  lssacsex  19910  lspsnat  19911  lsppratlem2  19914  lsppratlem3  19915  lsppratlem4  19916  lsppratlem6  19918  lspprat  19919  islbs2  19920  islbs3  19921  lbsacsbs  19922  lbsextlem2  19925  lbsextlem3  19926  lbsextlem4  19927  phllmod  20768  isphld  20792  islinds4  20973  lvecisfrlm  20981  cvsi  23728  0nellinds  30930  lindssn  30934  linds2eq  30936  lvecdim0i  30999  lssdimle  31001  tngdim  31006  matdim  31008  lbslsat  31009  lsatdim  31010  drngdimgt0  31011  lindsunlem  31015  lindsun  31016  lbsdiflsp0  31017  dimkerim  31018  qusdimsum  31019  fedgmullem1  31020  fedgmullem2  31021  fedgmul  31022  extdg1id  31048  ccfldextdgrr  31052  lindsadd  34879  lshpnelb  36114  lshpnel2N  36115  lshpdisj  36117  lshpcmp  36118  lsatcmp  36133  lsatcmp2  36134  lsatel  36135  lsatelbN  36136  lsatfixedN  36139  lsmcv2  36159  lsatcv0  36161  lsatcveq0  36162  lsat0cv  36163  lcvp  36170  lcv1  36171  lcv2  36172  lsatexch  36173  lsatnem0  36175  lsatexch1  36176  lsatcv0eq  36177  lsatcv1  36178  lsatcvatlem  36179  lsatcvat  36180  lsatcvat2  36181  lsatcvat3  36182  islshpcv  36183  l1cvpat  36184  l1cvat  36185  lfl1  36200  lkrsc  36227  lkrscss  36228  eqlkr  36229  eqlkr3  36231  lkrlsp  36232  lkrlsp3  36234  lkrshp  36235  lkrshp3  36236  lkrshpor  36237  lkrshp4  36238  lshpsmreu  36239  lshpkrlem1  36240  lshpkrlem4  36243  lshpkrlem5  36244  lshpkrlem6  36245  lshpkr  36247  lshpkrex  36248  lfl1dim  36251  lfl1dim2N  36252  lduallvec  36284  lduallkr3  36292  lkrpssN  36293  ldual1dim  36296  lkrss2N  36299  lkreqN  36300  lkrlspeqN  36301  dva0g  38157  dia1dim2  38192  dia1dimid  38193  dia2dimlem5  38198  dia2dimlem7  38200  dia2dimlem9  38202  dia2dimlem10  38203  dia2dimlem13  38206  dvhlmod  38240  diblsmopel  38301  lclkrlem2m  38649  lclkrlem2n  38650  lcfrlem1  38672  lcfrlem2  38673  lcfrlem3  38674  lcdlmod  38722  baerlem3lem1  38837  baerlem5alem1  38838  baerlem5blem1  38839  baerlem3lem2  38840  baerlem5alem2  38841  baerlem5blem2  38842  baerlem5amN  38846  baerlem5bmN  38847  baerlem5abmN  38848  mapdindp0  38849  mapdindp1  38850  mapdindp2  38851  mapdindp3  38852  mapdindp4  38853  lspindp5  38900  lvecgrp  39139  lvecring  39140  prjspersym  39250  prjsper  39251  prjspreln0  39252  prjspvs  39253  prjspeclsp  39255  0prjspn  39263  lincreslvec3  44530  isldepslvec2  44533  lindssnlvec  44534  lvecpsslmod  44555