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 )