MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lveclmod Structured version   Unicode version

Theorem lveclmod 17731
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
StepHypRef Expression
1 eqid 2443 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 17729 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 460 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   ` cfv 5578  Scalarcsca 14682   DivRingcdr 17375   LModclmod 17491   LVecclvec 17727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-lvec 17728
This theorem is referenced by:  lsslvec  17732  lvecvs0or  17733  lssvs0or  17735  lvecvscan  17736  lvecvscan2  17737  lvecinv  17738  lspsnvs  17739  lspsneleq  17740  lspsncmp  17741  lspsnne1  17742  lspsnnecom  17744  lspabs2  17745  lspabs3  17746  lspsneq  17747  lspsnel4  17749  lspdisj  17750  lspdisjb  17751  lspdisj2  17752  lspfixed  17753  lspexch  17754  lspexchn1  17755  lspindpi  17757  lvecindp  17763  lvecindp2  17764  lsmcv  17766  lspsolv  17768  lssacsex  17769  lspsnat  17770  lsppratlem2  17773  lsppratlem3  17774  lsppratlem4  17775  lsppratlem6  17777  lspprat  17778  islbs2  17779  islbs3  17780  lbsacsbs  17781  lbsextlem2  17784  lbsextlem3  17785  lbsextlem4  17786  phllmod  18643  isphld  18667  islinds4  18848  lvecisfrlm  18856  lincreslvec3  32953  isldepslvec2  32956  lindssnlvec  32957  lvecpsslmod  32978  lshpnelb  34584  lshpnel2N  34585  lshpdisj  34587  lshpcmp  34588  lsatcmp  34603  lsatcmp2  34604  lsatel  34605  lsatelbN  34606  lsatfixedN  34609  lsmcv2  34629  lsatcv0  34631  lsatcveq0  34632  lsat0cv  34633  lcvp  34640  lcv1  34641  lcv2  34642  lsatexch  34643  lsatnem0  34645  lsatexch1  34646  lsatcv0eq  34647  lsatcv1  34648  lsatcvatlem  34649  lsatcvat  34650  lsatcvat2  34651  lsatcvat3  34652  islshpcv  34653  l1cvpat  34654  l1cvat  34655  lfl1  34670  lkrsc  34697  lkrscss  34698  eqlkr  34699  eqlkr3  34701  lkrlsp  34702  lkrlsp3  34704  lkrshp  34705  lkrshp3  34706  lkrshpor  34707  lkrshp4  34708  lshpsmreu  34709  lshpkrlem1  34710  lshpkrlem4  34713  lshpkrlem5  34714  lshpkrlem6  34715  lshpkr  34717  lshpkrex  34718  lfl1dim  34721  lfl1dim2N  34722  lduallvec  34754  lduallkr3  34762  lkrpssN  34763  ldual1dim  34766  lkrss2N  34769  lkreqN  34770  lkrlspeqN  34771  dva0g  36629  dia1dim2  36664  dia1dimid  36665  dia2dimlem5  36670  dia2dimlem7  36672  dia2dimlem9  36674  dia2dimlem10  36675  dia2dimlem13  36678  dvhlmod  36712  diblsmopel  36773  lclkrlem2m  37121  lclkrlem2n  37122  lcfrlem1  37144  lcfrlem2  37145  lcfrlem3  37146  lcdlmod  37194  baerlem3lem1  37309  baerlem5alem1  37310  baerlem5blem1  37311  baerlem3lem2  37312  baerlem5alem2  37313  baerlem5blem2  37314  baerlem5amN  37318  baerlem5bmN  37319  baerlem5abmN  37320  mapdindp0  37321  mapdindp1  37322  mapdindp2  37323  mapdindp3  37324  mapdindp4  37325  lspindp5  37372
  Copyright terms: Public domain W3C validator