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

Metamath Proof Explorer

Theorem hhip

Description: The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 
|- U = <. <. +h , .h >. , normh >.
Assertion hhip 
|- .ih = ( .iOLD ` U )

Proof

Step Hyp Ref Expression
1 hhnv.1 
 |-  U = <. <. +h , .h >. , normh >.
2 polid 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih y ) = ( ( ( ( ( normh ` ( x +h y ) ) ^ 2 ) - ( ( normh ` ( x -h y ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( x +h ( _i .h y ) ) ) ^ 2 ) - ( ( normh ` ( x -h ( _i .h y ) ) ) ^ 2 ) ) ) ) / 4 ) )
3 1 hhnv 
 |-  U e. NrmCVec
4 1 hhba 
 |-  ~H = ( BaseSet ` U )
5 1 hhva 
 |-  +h = ( +v ` U )
6 1 hhsm 
 |-  .h = ( .sOLD ` U )
7 1 hhnm 
 |-  normh = ( normCV ` U )
8 eqid 
 |-  ( .iOLD ` U ) = ( .iOLD ` U )
9 1 hhvs 
 |-  -h = ( -v ` U )
10 4 5 6 7 8 9 ipval3 
 |-  ( ( U e. NrmCVec /\ x e. ~H /\ y e. ~H ) -> ( x ( .iOLD ` U ) y ) = ( ( ( ( ( normh ` ( x +h y ) ) ^ 2 ) - ( ( normh ` ( x -h y ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( x +h ( _i .h y ) ) ) ^ 2 ) - ( ( normh ` ( x -h ( _i .h y ) ) ) ^ 2 ) ) ) ) / 4 ) )
11 3 10 mp3an1 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x ( .iOLD ` U ) y ) = ( ( ( ( ( normh ` ( x +h y ) ) ^ 2 ) - ( ( normh ` ( x -h y ) ) ^ 2 ) ) + ( _i x. ( ( ( normh ` ( x +h ( _i .h y ) ) ) ^ 2 ) - ( ( normh ` ( x -h ( _i .h y ) ) ) ^ 2 ) ) ) ) / 4 ) )
12 2 11 eqtr4d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih y ) = ( x ( .iOLD ` U ) y ) )
13 12 rgen2 
 |-  A. x e. ~H A. y e. ~H ( x .ih y ) = ( x ( .iOLD ` U ) y )
14 ax-hfi 
 |-  .ih : ( ~H X. ~H ) --> CC
15 4 8 ipf 
 |-  ( U e. NrmCVec -> ( .iOLD ` U ) : ( ~H X. ~H ) --> CC )
16 3 15 ax-mp 
 |-  ( .iOLD ` U ) : ( ~H X. ~H ) --> CC
17 ffn 
 |-  ( .ih : ( ~H X. ~H ) --> CC -> .ih Fn ( ~H X. ~H ) )
18 ffn 
 |-  ( ( .iOLD ` U ) : ( ~H X. ~H ) --> CC -> ( .iOLD ` U ) Fn ( ~H X. ~H ) )
19 eqfnov2 
 |-  ( ( .ih Fn ( ~H X. ~H ) /\ ( .iOLD ` U ) Fn ( ~H X. ~H ) ) -> ( .ih = ( .iOLD ` U ) <-> A. x e. ~H A. y e. ~H ( x .ih y ) = ( x ( .iOLD ` U ) y ) ) )
20 17 18 19 syl2an 
 |-  ( ( .ih : ( ~H X. ~H ) --> CC /\ ( .iOLD ` U ) : ( ~H X. ~H ) --> CC ) -> ( .ih = ( .iOLD ` U ) <-> A. x e. ~H A. y e. ~H ( x .ih y ) = ( x ( .iOLD ` U ) y ) ) )
21 14 16 20 mp2an 
 |-  ( .ih = ( .iOLD ` U ) <-> A. x e. ~H A. y e. ~H ( x .ih y ) = ( x ( .iOLD ` U ) y ) )
22 13 21 mpbir 
 |-  .ih = ( .iOLD ` U )