This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlipf

Description: Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlipf.1 ⊢ X = BaseSet ⁡ U
hlipf.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion hlipf ⊢ U ∈ CHil OLD → P : X × X ⟶ ℂ

Proof

Step Hyp Ref Expression
1 hlipf.1 ⊢ X = BaseSet ⁡ U
2 hlipf.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
4 1 2 ipf ⊢ U ∈ NrmCVec → P : X × X ⟶ ℂ
5 3 4 syl ⊢ U ∈ CHil OLD → P : X × X ⟶ ℂ