Theorem phllmod 21671

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

Syntax hints:   → wi 4   ∈ wcel 2108  LModclmod 20880  LVecclvec 21124  PreHilcphl 21665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-iota 6525  df-fv 6581  df-ov 7451  df-lvec 21125  df-phl 21667

This theorem is referenced by:  iporthcom  21676  ip0l  21677  ip0r  21678  ipdir  21680  ipdi  21681  ip2di  21682  ipsubdir  21683  ipsubdi  21684  ip2subdi  21685  ipass  21686  ipassr  21687  ip2eq  21694  phssip  21699  phlssphl  21700  ocvlss  21713  ocvin  21715  ocvlsp  21717  ocvz  21719  ocv1  21720  lsmcss  21733  pjdm2  21754  pjff  21755  pjf2  21757  pjfo  21758  ocvpj  21760  obselocv  21771  obslbs  21773  phclm  25285  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  tcphcph  25290  pjth  25492