Theorem phllmod 21655

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

Syntax hints:   → wi 4   ∈ wcel 2136  LModclmod 20900  LVecclvec 21142  PreHilcphl 21649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-iota 6466  df-fv 6518  df-ov 7388  df-lvec 21143  df-phl 21651

This theorem is referenced by:  iporthcom  21660  ip0l  21661  ip0r  21662  ipdir  21664  ipdi  21665  ip2di  21666  ipsubdir  21667  ipsubdi  21668  ip2subdi  21669  ipass  21670  ipassr  21671  ip2eq  21678  phssip  21683  phlssphl  21684  ocvlss  21697  ocvin  21699  ocvlsp  21701  ocvz  21703  ocv1  21704  lsmcss  21717  pjdm2  21736  pjff  21737  pjf2  21739  pjfo  21740  ocvpj  21742  obselocv  21753  obslbs  21755  phclm  25267  ipcau2  25269  tcphcphlem1  25270  tcphcphlem2  25271  tcphcph  25272  pjth  25474