Theorem phllmod 20774

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

Syntax hints:   → wi 4   ∈ wcel 2114  LModclmod 19634  LVecclvec 19874  PreHilcphl 20768

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-iota 6314  df-fv 6363  df-ov 7159  df-lvec 19875  df-phl 20770

This theorem is referenced by:  iporthcom  20779  ip0l  20780  ip0r  20781  ipdir  20783  ipdi  20784  ip2di  20785  ipsubdir  20786  ipsubdi  20787  ip2subdi  20788  ipass  20789  ipassr  20790  ip2eq  20797  phssip  20802  phlssphl  20803  ocvlss  20816  ocvin  20818  ocvlsp  20820  ocvz  20822  ocv1  20823  lsmcss  20836  pjdm2  20855  pjff  20856  pjf2  20858  pjfo  20859  ocvpj  20861  obselocv  20872  obslbs  20874  phclm  23835  ipcau2  23837  tcphcphlem1  23838  tcphcphlem2  23839  tcphcph  23840  pjth  24042