This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )