Theorem phllmod 20823

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

Syntax hints:   → wi 4   ∈ wcel 2106  LModclmod 20111  LVecclvec 20352  PreHilcphl 20817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5229

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3432  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5158  df-iota 6385  df-fv 6435  df-ov 7271  df-lvec 20353  df-phl 20819

This theorem is referenced by:  iporthcom  20828  ip0l  20829  ip0r  20830  ipdir  20832  ipdi  20833  ip2di  20834  ipsubdir  20835  ipsubdi  20836  ip2subdi  20837  ipass  20838  ipassr  20839  ip2eq  20846  phssip  20851  phlssphl  20852  ocvlss  20865  ocvin  20867  ocvlsp  20869  ocvz  20871  ocv1  20872  lsmcss  20885  pjdm2  20906  pjff  20907  pjf2  20909  pjfo  20910  ocvpj  20912  obselocv  20923  obslbs  20925  phclm  24384  ipcau2  24386  tcphcphlem1  24387  tcphcphlem2  24388  tcphcph  24389  pjth  24591