Theorem hilims

Description: Hilbert space distance metric. (Contributed by NM, 13-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilims.1	|- ~H = ( BaseSet ` U )
	hilims.2	|- +h = ( +v ` U )
	hilims.3	|- .h = ( .sOLD ` U )
	hilims.5	|- .ih = ( .iOLD ` U )
	hilims.8	|- D = ( IndMet ` U )
	hilims.9	|- U e. NrmCVec
Assertion	hilims	|- D = ( normh o. -h )

Proof

Step	Hyp	Ref	Expression
1		hilims.1	|- ~H = ( BaseSet ` U )
2		hilims.2	|- +h = ( +v ` U )
3		hilims.3	|- .h = ( .sOLD ` U )
4		hilims.5	|- .ih = ( .iOLD ` U )
5		hilims.8	|- D = ( IndMet ` U )
6		hilims.9	|- U e. NrmCVec
7	1 2 3 4 6	hilhhi	|- U = <. <. +h , .h >. , normh >.
8	7 5	hhims2	|- D = ( normh o. -h )