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

Theorem lveclmod 17530
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 2462 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 17528 . 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 1762   ` cfv 5581  Scalarcsca 14549   DivRingcdr 17174   LModclmod 17290   LVecclvec 17526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-lvec 17527
This theorem is referenced by:  lsslvec  17531  lvecvs0or  17532  lssvs0or  17534  lvecvscan  17535  lvecvscan2  17536  lvecinv  17537  lspsnvs  17538  lspsneleq  17539  lspsncmp  17540  lspsnne1  17541  lspsnnecom  17543  lspabs2  17544  lspabs3  17545  lspsneq  17546  lspsnel4  17548  lspdisj  17549  lspdisjb  17550  lspdisj2  17551  lspfixed  17552  lspexch  17553  lspexchn1  17554  lspindpi  17556  lvecindp  17562  lvecindp2  17563  lsmcv  17565  lspsolv  17567  lssacsex  17568  lspsnat  17569  lsppratlem2  17572  lsppratlem3  17573  lsppratlem4  17574  lsppratlem6  17576  lspprat  17577  islbs2  17578  islbs3  17579  lbsacsbs  17580  lbsextlem2  17583  lbsextlem3  17584  lbsextlem4  17585  phllmod  18427  isphld  18451  islinds4  18632  lvecisfrlm  18640  lincreslvec3  32033  isldepslvec2  32036  lindssnlvec  32037  lvecpsslmod  32066  lshpnelb  33658  lshpnel2N  33659  lshpdisj  33661  lshpcmp  33662  lsatcmp  33677  lsatcmp2  33678  lsatel  33679  lsatelbN  33680  lsatfixedN  33683  lsmcv2  33703  lsatcv0  33705  lsatcveq0  33706  lsat0cv  33707  lcvp  33714  lcv1  33715  lcv2  33716  lsatexch  33717  lsatnem0  33719  lsatexch1  33720  lsatcv0eq  33721  lsatcv1  33722  lsatcvatlem  33723  lsatcvat  33724  lsatcvat2  33725  lsatcvat3  33726  islshpcv  33727  l1cvpat  33728  l1cvat  33729  lfl1  33744  lkrsc  33771  lkrscss  33772  eqlkr  33773  eqlkr3  33775  lkrlsp  33776  lkrlsp3  33778  lkrshp  33779  lkrshp3  33780  lkrshpor  33781  lkrshp4  33782  lshpsmreu  33783  lshpkrlem1  33784  lshpkrlem4  33787  lshpkrlem5  33788  lshpkrlem6  33789  lshpkr  33791  lshpkrex  33792  lfl1dim  33795  lfl1dim2N  33796  lduallvec  33828  lduallkr3  33836  lkrpssN  33837  ldual1dim  33840  lkrss2N  33843  lkreqN  33844  lkrlspeqN  33845  dva0g  35701  dia1dim2  35736  dia1dimid  35737  dia2dimlem5  35742  dia2dimlem7  35744  dia2dimlem9  35746  dia2dimlem10  35747  dia2dimlem13  35750  dvhlmod  35784  diblsmopel  35845  lclkrlem2m  36193  lclkrlem2n  36194  lcfrlem1  36216  lcfrlem2  36217  lcfrlem3  36218  lcdlmod  36266  baerlem3lem1  36381  baerlem5alem1  36382  baerlem5blem1  36383  baerlem3lem2  36384  baerlem5alem2  36385  baerlem5blem2  36386  baerlem5amN  36390  baerlem5bmN  36391  baerlem5abmN  36392  mapdindp0  36393  mapdindp1  36394  mapdindp2  36395  mapdindp3  36396  mapdindp4  36397  lspindp5  36444
  Copyright terms: Public domain W3C validator