Theorem phllmod 20177

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

Syntax hints:   → wi 4   ∈ wcel 2139  LModclmod 19065  LVecclvec 19304  PreHilcphl 20171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-iota 6012  df-fv 6057  df-ov 6816  df-lvec 19305  df-phl 20173

This theorem is referenced by:  iporthcom  20182  ip0l  20183  ip0r  20184  ipdir  20186  ipdi  20187  ip2di  20188  ipsubdir  20189  ipsubdi  20190  ip2subdi  20191  ipass  20192  ipassr  20193  ip2eq  20200  phssip  20205  ocvlss  20218  ocvin  20220  ocvlsp  20222  ocvz  20224  ocv1  20225  lsmcss  20238  pjdm2  20257  pjff  20258  pjf2  20260  pjfo  20261  ocvpj  20263  obselocv  20274  obslbs  20276  tchclm  23231  ipcau2  23233  tchcphlem1  23234  tchcphlem2  23235  tchcph  23236  pjth  23410