Theorem lveclmod 19106

Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)

Assertion

Ref	Expression
lveclmod	|- ( W e. LVec -> W e. LMod )

Proof of Theorem lveclmod

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- (Scalar ` W ) = (Scalar ` W )
2	1	islvec 19104	. 2 |- ( W e. LVec <-> ( W e. LMod /\ (Scalar ` W ) e. DivRing ) )
3	2	simplbi 476	1 |- ( W e. LVec -> W e. LMod )

Syntax hints:   -> wi 4   e. wcel 1990   ` cfv 5888  Scalarcsca 15944   DivRingcdr 18747   LModclmod 18863   LVecclvec 19102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-lvec 19103

This theorem is referenced by:  lsslvec  19107  lvecvs0or  19108  lssvs0or  19110  lvecvscan  19111  lvecvscan2  19112  lvecinv  19113  lspsnvs  19114  lspsneleq  19115  lspsncmp  19116  lspsnne1  19117  lspsnnecom  19119  lspabs2  19120  lspabs3  19121  lspsneq  19122  lspsnel4  19124  lspdisj  19125  lspdisjb  19126  lspdisj2  19127  lspfixed  19128  lspexch  19129  lspexchn1  19130  lspindpi  19132  lvecindp  19138  lvecindp2  19139  lsmcv  19141  lspsolv  19143  lssacsex  19144  lspsnat  19145  lsppratlem2  19148  lsppratlem3  19149  lsppratlem4  19150  lsppratlem6  19152  lspprat  19153  islbs2  19154  islbs3  19155  lbsacsbs  19156  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  phllmod  19975  isphld  19999  islinds4  20174  lvecisfrlm  20182  cvsi  22930  lshpnelb  34271  lshpnel2N  34272  lshpdisj  34274  lshpcmp  34275  lsatcmp  34290  lsatcmp2  34291  lsatel  34292  lsatelbN  34293  lsatfixedN  34296  lsmcv2  34316  lsatcv0  34318  lsatcveq0  34319  lsat0cv  34320  lcvp  34327  lcv1  34328  lcv2  34329  lsatexch  34330  lsatnem0  34332  lsatexch1  34333  lsatcv0eq  34334  lsatcv1  34335  lsatcvatlem  34336  lsatcvat  34337  lsatcvat2  34338  lsatcvat3  34339  islshpcv  34340  l1cvpat  34341  l1cvat  34342  lfl1  34357  lkrsc  34384  lkrscss  34385  eqlkr  34386  eqlkr3  34388  lkrlsp  34389  lkrlsp3  34391  lkrshp  34392  lkrshp3  34393  lkrshpor  34394  lkrshp4  34395  lshpsmreu  34396  lshpkrlem1  34397  lshpkrlem4  34400  lshpkrlem5  34401  lshpkrlem6  34402  lshpkr  34404  lshpkrex  34405  lfl1dim  34408  lfl1dim2N  34409  lduallvec  34441  lduallkr3  34449  lkrpssN  34450  ldual1dim  34453  lkrss2N  34456  lkreqN  34457  lkrlspeqN  34458  dva0g  36316  dia1dim2  36351  dia1dimid  36352  dia2dimlem5  36357  dia2dimlem7  36359  dia2dimlem9  36361  dia2dimlem10  36362  dia2dimlem13  36365  dvhlmod  36399  diblsmopel  36460  lclkrlem2m  36808  lclkrlem2n  36809  lcfrlem1  36831  lcfrlem2  36832  lcfrlem3  36833  lcdlmod  36881  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdindp0  37008  mapdindp1  37009  mapdindp2  37010  mapdindp3  37011  mapdindp4  37012  lspindp5  37059  lincreslvec3  42271  isldepslvec2  42274  lindssnlvec  42275  lvecpsslmod  42296