Theorem phllmod 21847

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  LModclmod 21048  LVecclvec 21290  PreHilcphl 21841

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-iota 6493  df-fv 6545  df-ov 7419  df-lvec 21291  df-phl 21843

This theorem is used by:  iporthcom  21852  ip0l  21853  ip0r  21854  ipdir  21856  ipdi  21857  ip2di  21858  ipsubdir  21859  ipsubdi  21860  ip2subdi  21861  ipass  21862  ipassr  21863  ip2eq  21870  phssip  21875  phlssphl  21876  ocvlss  21889  ocvin  21891  ocvlsp  21893  ocvz  21895  ocv1  21896  lsmcss  21909  pjdm2  21928  pjff  21929  pjf2  21931  pjfo  21932  ocvpj  21934  obselocv  21945  obslbs  21947  phclm  25464  ipcau2  25466  tcphcphlem1  25467  tcphcphlem2  25468  tcphcph  25469  pjth  25671