Theorem phllmod 21618

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

Syntax hints:   → wi 4   ∈ wcel 2114  LModclmod 20844  LVecclvec 21087  PreHilcphl 21612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-iota 6446  df-fv 6498  df-ov 7361  df-lvec 21088  df-phl 21614

This theorem is referenced by:  iporthcom  21623  ip0l  21624  ip0r  21625  ipdir  21627  ipdi  21628  ip2di  21629  ipsubdir  21630  ipsubdi  21631  ip2subdi  21632  ipass  21633  ipassr  21634  ip2eq  21641  phssip  21646  phlssphl  21647  ocvlss  21660  ocvin  21662  ocvlsp  21664  ocvz  21666  ocv1  21667  lsmcss  21680  pjdm2  21699  pjff  21700  pjf2  21702  pjfo  21703  ocvpj  21705  obselocv  21716  obslbs  21718  phclm  25208  ipcau2  25210  tcphcphlem1  25211  tcphcphlem2  25212  tcphcph  25213  pjth  25415