Theorem phllmod 21555

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 21554	. 2 ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
2		lveclmod 21028	. 2 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∈ wcel 2109  LModclmod 20781  LVecclvec 21024  PreHilcphl 21549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-iota 6442  df-fv 6494  df-ov 7356  df-lvec 21025  df-phl 21551

This theorem is referenced by:  iporthcom  21560  ip0l  21561  ip0r  21562  ipdir  21564  ipdi  21565  ip2di  21566  ipsubdir  21567  ipsubdi  21568  ip2subdi  21569  ipass  21570  ipassr  21571  ip2eq  21578  phssip  21583  phlssphl  21584  ocvlss  21597  ocvin  21599  ocvlsp  21601  ocvz  21603  ocv1  21604  lsmcss  21617  pjdm2  21636  pjff  21637  pjf2  21639  pjfo  21640  ocvpj  21642  obselocv  21653  obslbs  21655  phclm  25148  ipcau2  25150  tcphcphlem1  25151  tcphcphlem2  25152  tcphcph  25153  pjth  25355