Metamath Proof Explorer

Theorem hlphl

Description: Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion hlphl ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ PreHil )

Proof

Step Hyp Ref Expression
1 hlcph ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ β„‚PreHil )
2 cphphl ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )
3 1 2 syl ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ PreHil )