Theorem phllmod 19975

Description: A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)

Assertion

Ref	Expression
phllmod	|- ( W e. PreHil -> W e. LMod )

Proof of Theorem phllmod

Step	Hyp	Ref	Expression
1		phllvec 19974	. 2 |- ( W e. PreHil -> W e. LVec )
2		lveclmod 19106	. 2 |- ( W e. LVec -> W e. LMod )
3	1, 2	syl 17	1 |- ( W e. PreHil -> W e. LMod )

Syntax hints:   -> wi 4   e. wcel 1990   LModclmod 18863   LVecclvec 19102   PreHilcphl 19969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-iota 5851  df-fv 5896  df-ov 6653  df-lvec 19103  df-phl 19971

This theorem is referenced by:  iporthcom  19980  ip0l  19981  ip0r  19982  ipdir  19984  ipdi  19985  ip2di  19986  ipsubdir  19987  ipsubdi  19988  ip2subdi  19989  ipass  19990  ipassr  19991  ip2eq  19998  phssip  20003  ocvlss  20016  ocvin  20018  ocvlsp  20020  ocvz  20022  ocv1  20023  lsmcss  20036  pjdm2  20055  pjff  20056  pjf2  20058  pjfo  20059  ocvpj  20061  obselocv  20072  obslbs  20074  tchclm  23031  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  tchcph  23036  pjth  23210