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

Theorem lveclmod 18314
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 2422 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
21islvec 18312 . 2  |-  ( W  e.  LVec  <->  ( W  e. 
LMod  /\  (Scalar `  W
)  e.  DivRing ) )
32simplbi 461 1  |-  ( W  e.  LVec  ->  W  e. 
LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   ` cfv 5597  Scalarcsca 15178   DivRingcdr 17960   LModclmod 18076   LVecclvec 18310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-iota 5561  df-fv 5605  df-lvec 18311
This theorem is referenced by:  lsslvec  18315  lvecvs0or  18316  lssvs0or  18318  lvecvscan  18319  lvecvscan2  18320  lvecinv  18321  lspsnvs  18322  lspsneleq  18323  lspsncmp  18324  lspsnne1  18325  lspsnnecom  18327  lspabs2  18328  lspabs3  18329  lspsneq  18330  lspsnel4  18332  lspdisj  18333  lspdisjb  18334  lspdisj2  18335  lspfixed  18336  lspexch  18337  lspexchn1  18338  lspindpi  18340  lvecindp  18346  lvecindp2  18347  lsmcv  18349  lspsolv  18351  lssacsex  18352  lspsnat  18353  lsppratlem2  18356  lsppratlem3  18357  lsppratlem4  18358  lsppratlem6  18360  lspprat  18361  islbs2  18362  islbs3  18363  lbsacsbs  18364  lbsextlem2  18367  lbsextlem3  18368  lbsextlem4  18369  phllmod  19181  isphld  19205  islinds4  19377  lvecisfrlm  19385  lshpnelb  32466  lshpnel2N  32467  lshpdisj  32469  lshpcmp  32470  lsatcmp  32485  lsatcmp2  32486  lsatel  32487  lsatelbN  32488  lsatfixedN  32491  lsmcv2  32511  lsatcv0  32513  lsatcveq0  32514  lsat0cv  32515  lcvp  32522  lcv1  32523  lcv2  32524  lsatexch  32525  lsatnem0  32527  lsatexch1  32528  lsatcv0eq  32529  lsatcv1  32530  lsatcvatlem  32531  lsatcvat  32532  lsatcvat2  32533  lsatcvat3  32534  islshpcv  32535  l1cvpat  32536  l1cvat  32537  lfl1  32552  lkrsc  32579  lkrscss  32580  eqlkr  32581  eqlkr3  32583  lkrlsp  32584  lkrlsp3  32586  lkrshp  32587  lkrshp3  32588  lkrshpor  32589  lkrshp4  32590  lshpsmreu  32591  lshpkrlem1  32592  lshpkrlem4  32595  lshpkrlem5  32596  lshpkrlem6  32597  lshpkr  32599  lshpkrex  32600  lfl1dim  32603  lfl1dim2N  32604  lduallvec  32636  lduallkr3  32644  lkrpssN  32645  ldual1dim  32648  lkrss2N  32651  lkreqN  32652  lkrlspeqN  32653  dva0g  34511  dia1dim2  34546  dia1dimid  34547  dia2dimlem5  34552  dia2dimlem7  34554  dia2dimlem9  34556  dia2dimlem10  34557  dia2dimlem13  34560  dvhlmod  34594  diblsmopel  34655  lclkrlem2m  35003  lclkrlem2n  35004  lcfrlem1  35026  lcfrlem2  35027  lcfrlem3  35028  lcdlmod  35076  baerlem3lem1  35191  baerlem5alem1  35192  baerlem5blem1  35193  baerlem3lem2  35194  baerlem5alem2  35195  baerlem5blem2  35196  baerlem5amN  35200  baerlem5bmN  35201  baerlem5abmN  35202  mapdindp0  35203  mapdindp1  35204  mapdindp2  35205  mapdindp3  35206  mapdindp4  35207  lspindp5  35254  lincreslvec3  39463  isldepslvec2  39466  lindssnlvec  39467  lvecpsslmod  39488
  Copyright terms: Public domain W3C validator