Theorem phllmod 21597

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

Step	Hyp	Ref	Expression
1		phllvec 21596	. 2 ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
2		lveclmod 21070	. 2 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2114  LModclmod 20823  LVecclvec 21066  PreHilcphl 21591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-iota 6456  df-fv 6508  df-ov 7371  df-lvec 21067  df-phl 21593

This theorem is referenced by:  iporthcom  21602  ip0l  21603  ip0r  21604  ipdir  21606  ipdi  21607  ip2di  21608  ipsubdir  21609  ipsubdi  21610  ip2subdi  21611  ipass  21612  ipassr  21613  ip2eq  21620  phssip  21625  phlssphl  21626  ocvlss  21639  ocvin  21641  ocvlsp  21643  ocvz  21645  ocv1  21646  lsmcss  21659  pjdm2  21678  pjff  21679  pjf2  21681  pjfo  21682  ocvpj  21684  obselocv  21695  obslbs  21697  phclm  25200  ipcau2  25202  tcphcphlem1  25203  tcphcphlem2  25204  tcphcph  25205  pjth  25407