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

Theorem lveclmod 20582
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
StepHypRef Expression
1 eqid 2733 . . 3 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
21islvec 20580 . 2 (π‘Š ∈ LVec ↔ (π‘Š ∈ LMod ∧ (Scalarβ€˜π‘Š) ∈ DivRing))
32simplbi 499 1 (π‘Š ∈ LVec β†’ π‘Š ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∈ wcel 2107  β€˜cfv 6497  Scalarcsca 17141  DivRingcdr 20197  LModclmod 20336  LVecclvec 20578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-lvec 20579
This theorem is referenced by:  lveclmodd  20583  lsslvec  20584  lvecvs0or  20585  lssvs0or  20587  lvecvscan  20588  lvecvscan2  20589  lvecinv  20590  lspsnvs  20591  lspsneleq  20592  lspsncmp  20593  lspsnne1  20594  lspsnnecom  20596  lspabs2  20597  lspabs3  20598  lspsneq  20599  lspsnel4  20601  lspdisj  20602  lspdisjb  20603  lspdisj2  20604  lspfixed  20605  lspexch  20606  lspexchn1  20607  lspindpi  20609  lvecindp  20615  lvecindp2  20616  lsmcv  20618  lspsolv  20620  lssacsex  20621  lspsnat  20622  lsppratlem2  20625  lsppratlem3  20626  lsppratlem4  20627  lsppratlem6  20629  lspprat  20630  islbs2  20631  islbs3  20632  lbsacsbs  20633  lbsextlem2  20636  lbsextlem3  20637  lbsextlem4  20638  phllmod  21050  isphld  21074  islinds4  21257  lvecisfrlm  21265  cvsi  24509  0nellinds  32206  lindssn  32213  linds2eq  32216  lvecdim0i  32358  lssdimle  32360  tngdim  32365  matdim  32367  lbslsat  32368  lsatdim  32369  drngdimgt0  32370  lindsunlem  32376  lindsun  32377  lbsdiflsp0  32378  dimkerim  32379  qusdimsum  32380  fedgmullem1  32381  fedgmullem2  32382  fedgmul  32383  extdg1id  32409  ccfldextdgrr  32413  lindsadd  36117  lshpnelb  37492  lshpnel2N  37493  lshpdisj  37495  lshpcmp  37496  lsatcmp  37511  lsatcmp2  37512  lsatel  37513  lsatelbN  37514  lsatfixedN  37517  lsmcv2  37537  lsatcv0  37539  lsatcveq0  37540  lsat0cv  37541  lcvp  37548  lcv1  37549  lcv2  37550  lsatexch  37551  lsatnem0  37553  lsatexch1  37554  lsatcv0eq  37555  lsatcv1  37556  lsatcvatlem  37557  lsatcvat  37558  lsatcvat2  37559  lsatcvat3  37560  islshpcv  37561  l1cvpat  37562  l1cvat  37563  lfl1  37578  lkrsc  37605  lkrscss  37606  eqlkr  37607  eqlkr3  37609  lkrlsp  37610  lkrlsp3  37612  lkrshp  37613  lkrshp3  37614  lkrshpor  37615  lkrshp4  37616  lshpsmreu  37617  lshpkrlem1  37618  lshpkrlem4  37621  lshpkrlem5  37622  lshpkrlem6  37623  lshpkr  37625  lshpkrex  37626  lfl1dim  37629  lfl1dim2N  37630  lduallvec  37662  lduallkr3  37670  lkrpssN  37671  ldual1dim  37674  lkrss2N  37677  lkreqN  37678  lkrlspeqN  37679  dva0g  39536  dia1dim2  39571  dia1dimid  39572  dia2dimlem5  39577  dia2dimlem7  39579  dia2dimlem9  39581  dia2dimlem10  39582  dia2dimlem13  39585  dvhlmod  39619  diblsmopel  39680  lclkrlem2m  40028  lclkrlem2n  40029  lcfrlem1  40051  lcfrlem2  40052  lcfrlem3  40053  lcdlmod  40101  baerlem3lem1  40216  baerlem5alem1  40217  baerlem5blem1  40218  baerlem3lem2  40219  baerlem5alem2  40220  baerlem5blem2  40221  baerlem5amN  40225  baerlem5bmN  40226  baerlem5abmN  40227  mapdindp0  40228  mapdindp1  40229  mapdindp2  40230  mapdindp3  40231  mapdindp4  40232  lspindp5  40279  lvecgrp  40766  lvecring  40768  prjspersym  40988  prjsper  40989  prjspreln0  40990  prjspvs  40991  prjspeclsp  40993  0prjspn  41009  lincreslvec3  46649  isldepslvec2  46652  lindssnlvec  46653  lvecpsslmod  46674
  Copyright terms: Public domain W3C validator