Theorem phllmod 21539

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

Syntax hints:   → wi 4   ∈ wcel 2109  LModclmod 20766  LVecclvec 21009  PreHilcphl 21533

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 5261

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 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-iota 6464  df-fv 6519  df-ov 7390  df-lvec 21010  df-phl 21535

This theorem is referenced by:  iporthcom  21544  ip0l  21545  ip0r  21546  ipdir  21548  ipdi  21549  ip2di  21550  ipsubdir  21551  ipsubdi  21552  ip2subdi  21553  ipass  21554  ipassr  21555  ip2eq  21562  phssip  21567  phlssphl  21568  ocvlss  21581  ocvin  21583  ocvlsp  21585  ocvz  21587  ocv1  21588  lsmcss  21601  pjdm2  21620  pjff  21621  pjf2  21623  pjfo  21624  ocvpj  21626  obselocv  21637  obslbs  21639  phclm  25132  ipcau2  25134  tcphcphlem1  25135  tcphcphlem2  25136  tcphcph  25137  pjth  25339