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

Theorem phllmod 17901
Description: A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
Assertion
Ref Expression
phllmod  |-  ( W  e.  PreHil  ->  W  e.  LMod )

Proof of Theorem phllmod
StepHypRef Expression
1 phllvec 17900 . 2  |-  ( W  e.  PreHil  ->  W  e.  LVec )
2 lveclmod 17109 . 2  |-  ( W  e.  LVec  ->  W  e. 
LMod )
31, 2syl 16 1  |-  ( W  e.  PreHil  ->  W  e.  LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   LModclmod 16872   LVecclvec 17105   PreHilcphl 17895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-iota 5369  df-fv 5414  df-ov 6083  df-lvec 17106  df-phl 17897
This theorem is referenced by:  iporthcom  17906  ip0l  17907  ip0r  17908  ipdir  17910  ipdi  17911  ip2di  17912  ipsubdir  17913  ipsubdi  17914  ip2subdi  17915  ipass  17916  ipassr  17917  ip2eq  17924  ocvlss  17939  ocvin  17941  ocvlsp  17943  ocvz  17945  ocv1  17946  lsmcss  17959  pjdm2  17978  pjff  17979  pjf2  17981  pjfo  17982  ocvpj  17984  obselocv  17995  obslbs  17997  tchclm  20589  ipcau2  20591  tchcphlem1  20592  tchcphlem2  20593  tchcph  20594  pjth  20768
  Copyright terms: Public domain W3C validator