Theorem phllmod 21577

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

Syntax hints:   → wi 4   ∈ wcel 2107  LModclmod 20804  LVecclvec 21047  PreHilcphl 21571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5274

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rab 3414  df-v 3459  df-sbc 3764  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-iota 6481  df-fv 6536  df-ov 7403  df-lvec 21048  df-phl 21573

This theorem is referenced by:  iporthcom  21582  ip0l  21583  ip0r  21584  ipdir  21586  ipdi  21587  ip2di  21588  ipsubdir  21589  ipsubdi  21590  ip2subdi  21591  ipass  21592  ipassr  21593  ip2eq  21600  phssip  21605  phlssphl  21606  ocvlss  21619  ocvin  21621  ocvlsp  21623  ocvz  21625  ocv1  21626  lsmcss  21639  pjdm2  21658  pjff  21659  pjf2  21661  pjfo  21662  ocvpj  21664  obselocv  21675  obslbs  21677  phclm  25171  ipcau2  25173  tcphcphlem1  25174  tcphcphlem2  25175  tcphcph  25176  pjth  25378