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 = ( .iOLD ` U )
Assertion hlipf
|- ( U e. CHilOLD -> P : ( X X. X ) --> CC )

Proof

Step Hyp Ref Expression
1 hlipf.1
 |-  X = ( BaseSet ` U )
2 hlipf.7
 |-  P = ( .iOLD ` U )
3 hlnv
 |-  ( U e. CHilOLD -> U e. NrmCVec )
4 1 2 ipf
 |-  ( U e. NrmCVec -> P : ( X X. X ) --> CC )
5 3 4 syl
 |-  ( U e. CHilOLD -> P : ( X X. X ) --> CC )