Theorem hilhhi

Description: Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilhh.1	|- ~H = ( BaseSet ` U )
	hilhh.2	|- +h = ( +v ` U )
	hilhh.3	|- .h = ( .sOLD ` U )
	hilhh.5	|- .ih = ( .iOLD ` U )
	hilhh.9	|- U e. NrmCVec
Assertion	hilhhi	|- U = <. <. +h , .h >. , normh >.

Proof

Step	Hyp	Ref	Expression
1		hilhh.1	|- ~H = ( BaseSet ` U )
2		hilhh.2	|- +h = ( +v ` U )
3		hilhh.3	|- .h = ( .sOLD ` U )
4		hilhh.5	|- .ih = ( .iOLD ` U )
5		hilhh.9	|- U e. NrmCVec
6	1 4 5	hilnormi	|- normh = ( normCV ` U )
7	2 3 6	nvop	|- ( U e. NrmCVec -> U = <. <. +h , .h >. , normh >. )
8	5 7	ax-mp	|- U = <. <. +h , .h >. , normh >.