Theorem h2hsm

Description: The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2h.1	|- U = <. <. +h , .h >. , normh >.
	h2h.2	|- U e. NrmCVec
Assertion	h2hsm	|- .h = ( .sOLD ` U )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	|- U = <. <. +h , .h >. , normh >.
2		h2h.2	|- U e. NrmCVec
3		eqid	|- ( .sOLD ` <. <. +h , .h >. , normh >. ) = ( .sOLD ` <. <. +h , .h >. , normh >. )
4	3	smfval	|- ( .sOLD ` <. <. +h , .h >. , normh >. ) = ( 2nd ` ( 1st ` <. <. +h , .h >. , normh >. ) )
5		opex	|- <. +h , .h >. e. _V
6	1 2	eqeltrri	|- <. <. +h , .h >. , normh >. e. NrmCVec
7		nvex	|- ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( +h e. _V /\ .h e. _V /\ normh e. _V ) )
8	6 7	ax-mp	|- ( +h e. _V /\ .h e. _V /\ normh e. _V )
9	8	simp3i	|- normh e. _V
10	5 9	op1st	|- ( 1st ` <. <. +h , .h >. , normh >. ) = <. +h , .h >.
11	10	fveq2i	|- ( 2nd ` ( 1st ` <. <. +h , .h >. , normh >. ) ) = ( 2nd ` <. +h , .h >. )
12	8	simp1i	|- +h e. _V
13	8	simp2i	|- .h e. _V
14	12 13	op2nd	|- ( 2nd ` <. +h , .h >. ) = .h
15	4 11 14	3eqtrri	|- .h = ( .sOLD ` <. <. +h , .h >. , normh >. )
16	1	fveq2i	|- ( .sOLD ` U ) = ( .sOLD ` <. <. +h , .h >. , normh >. )
17	15 16	eqtr4i	|- .h = ( .sOLD ` U )