Theorem phllmod 21898

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  LModclmod 21097  LVecclvec 21339  PreHilcphl 21892

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 2147  ax-9 2155  ax-ext 2732  ax-nul 5259

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-iota 6483  df-fv 6535  df-ov 7411  df-lvec 21340  df-phl 21894

This theorem is used by:  iporthcom  21903  ip0l  21904  ip0r  21905  ipdir  21907  ipdi  21908  ip2di  21909  ipsubdir  21910  ipsubdi  21911  ip2subdi  21912  ipass  21913  ipassr  21914  ip2eq  21921  phssip  21926  phlssphl  21927  ocvlss  21940  ocvin  21942  ocvlsp  21944  ocvz  21946  ocv1  21947  lsmcss  21960  pjdm2  21979  pjff  21980  pjf2  21982  pjfo  21983  ocvpj  21985  obselocv  21996  obslbs  21998  phclm  25515  ipcau2  25517  tcphcphlem1  25518  tcphcphlem2  25519  tcphcph  25520  pjth  25722