Theorem phllmod 21566

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

Syntax hints:   → wi 4   ∈ wcel 2098  LModclmod 20747  LVecclvec 20991  PreHilcphl 21560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3465  df-sbc 3775  df-dif 3948  df-un 3950  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-iota 6499  df-fv 6555  df-ov 7420  df-lvec 20992  df-phl 21562

This theorem is referenced by:  iporthcom  21571  ip0l  21572  ip0r  21573  ipdir  21575  ipdi  21576  ip2di  21577  ipsubdir  21578  ipsubdi  21579  ip2subdi  21580  ipass  21581  ipassr  21582  ip2eq  21589  phssip  21594  phlssphl  21595  ocvlss  21608  ocvin  21610  ocvlsp  21612  ocvz  21614  ocv1  21615  lsmcss  21628  pjdm2  21649  pjff  21650  pjf2  21652  pjfo  21653  ocvpj  21655  obselocv  21666  obslbs  21668  phclm  25190  ipcau2  25192  tcphcphlem1  25193  tcphcphlem2  25194  tcphcph  25195  pjth  25397