Theorem phllmod 20373

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

Syntax hints:   → wi 4   ∈ wcel 2106  LModclmod 19255  LVecclvec 19497  PreHilcphl 20367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-nul 5025

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-iota 6099  df-fv 6143  df-ov 6925  df-lvec 19498  df-phl 20369

This theorem is referenced by:  iporthcom  20378  ip0l  20379  ip0r  20380  ipdir  20382  ipdi  20383  ip2di  20384  ipsubdir  20385  ipsubdi  20386  ip2subdi  20387  ipass  20388  ipassr  20389  ip2eq  20396  phssip  20401  phlssphl  20402  ocvlss  20415  ocvin  20417  ocvlsp  20419  ocvz  20421  ocv1  20422  lsmcss  20435  pjdm2  20454  pjff  20455  pjf2  20457  pjfo  20458  ocvpj  20460  obselocv  20471  obslbs  20473  phclm  23438  ipcau2  23440  tcphcphlem1  23441  tcphcphlem2  23442  tcphcph  23443  pjth  23645