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

Theorem phllmod 21057
Description: A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
Assertion
Ref Expression
phllmod (𝑊 ∈ PreHil → 𝑊 ∈ LMod)

Proof of Theorem phllmod
StepHypRef Expression
1 phllvec 21056 . 2 (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
2 lveclmod 20611 . 2 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
31, 2syl 17 1 (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  LModclmod 20365  LVecclvec 20607  PreHilcphl 21051
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  ax-nul 5267
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-ne 2941  df-ral 3062  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-iota 6452  df-fv 6508  df-ov 7364  df-lvec 20608  df-phl 21053
This theorem is referenced by:  iporthcom  21062  ip0l  21063  ip0r  21064  ipdir  21066  ipdi  21067  ip2di  21068  ipsubdir  21069  ipsubdi  21070  ip2subdi  21071  ipass  21072  ipassr  21073  ip2eq  21080  phssip  21085  phlssphl  21086  ocvlss  21099  ocvin  21101  ocvlsp  21103  ocvz  21105  ocv1  21106  lsmcss  21119  pjdm2  21140  pjff  21141  pjf2  21143  pjfo  21144  ocvpj  21146  obselocv  21157  obslbs  21159  phclm  24619  ipcau2  24621  tcphcphlem1  24622  tcphcphlem2  24623  tcphcph  24624  pjth  24826
  Copyright terms: Public domain W3C validator