Theorem phllmod 21810

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  LModclmod 21011  LVecclvec 21253  PreHilcphl 21804

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-iota 6499  df-fv 6551  df-ov 7426  df-lvec 21254  df-phl 21806

This theorem is used by:  iporthcom  21815  ip0l  21816  ip0r  21817  ipdir  21819  ipdi  21820  ip2di  21821  ipsubdir  21822  ipsubdi  21823  ip2subdi  21824  ipass  21825  ipassr  21826  ip2eq  21833  phssip  21838  phlssphl  21839  ocvlss  21852  ocvin  21854  ocvlsp  21856  ocvz  21858  ocv1  21859  lsmcss  21872  pjdm2  21891  pjff  21892  pjf2  21894  pjfo  21895  ocvpj  21897  obselocv  21908  obslbs  21910  phclm  25421  ipcau2  25423  tcphcphlem1  25424  tcphcphlem2  25425  tcphcph  25426  pjth  25628