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 )