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

Syntax hints:   → wi 4   ∈ wcel 2113  LModclmod 20803  LVecclvec 21046  PreHilcphl 21571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-iota 6445  df-fv 6497  df-ov 7358  df-lvec 21047  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  25169  ipcau2  25171  tcphcphlem1  25172  tcphcphlem2  25173  tcphcph  25174  pjth  25376