Theorem phllmod 21612

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

Syntax hints:   → wi 4   ∈ wcel 2119  LModclmod 20857  LVecclvec 21099  PreHilcphl 21606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-iota 6448  df-fv 6500  df-ov 7366  df-lvec 21100  df-phl 21608

This theorem is referenced by:  iporthcom  21617  ip0l  21618  ip0r  21619  ipdir  21621  ipdi  21622  ip2di  21623  ipsubdir  21624  ipsubdi  21625  ip2subdi  21626  ipass  21627  ipassr  21628  ip2eq  21635  phssip  21640  phlssphl  21641  ocvlss  21654  ocvin  21656  ocvlsp  21658  ocvz  21660  ocv1  21661  lsmcss  21674  pjdm2  21693  pjff  21694  pjf2  21696  pjfo  21697  ocvpj  21699  obselocv  21710  obslbs  21712  phclm  25224  ipcau2  25226  tcphcphlem1  25227  tcphcphlem2  25228  tcphcph  25229  pjth  25431