Metamath Proof Explorer

Theorem hhph

Description: The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 
|- U = <. <. +h , .h >. , normh >.
Assertion hhph 
|- U e. CPreHilOLD

Proof

Step Hyp Ref Expression
1 hhnv.1 
 |-  U = <. <. +h , .h >. , normh >.
2 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
3 2 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
4 normpar 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( normh ` ( x -h y ) ) ^ 2 ) + ( ( normh ` ( x +h y ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` x ) ^ 2 ) ) + ( 2 x. ( ( normh ` y ) ^ 2 ) ) ) )
5 hvsubval 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x -h y ) = ( x +h ( -u 1 .h y ) ) )
6 5 fveq2d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x -h y ) ) = ( normh ` ( x +h ( -u 1 .h y ) ) ) )
7 6 oveq1d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( normh ` ( x -h y ) ) ^ 2 ) = ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) )
8 7 oveq2d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x -h y ) ) ^ 2 ) ) = ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) )
9 hvaddcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H )
10 normcl 
 |-  ( ( x +h y ) e. ~H -> ( normh ` ( x +h y ) ) e. RR )
11 9 10 syl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x +h y ) ) e. RR )
12 11 recnd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x +h y ) ) e. CC )
13 12 sqcld 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( normh ` ( x +h y ) ) ^ 2 ) e. CC )
14 hvsubcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x -h y ) e. ~H )
15 normcl 
 |-  ( ( x -h y ) e. ~H -> ( normh ` ( x -h y ) ) e. RR )
16 15 recnd 
 |-  ( ( x -h y ) e. ~H -> ( normh ` ( x -h y ) ) e. CC )
17 14 16 syl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x -h y ) ) e. CC )
18 17 sqcld 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( normh ` ( x -h y ) ) ^ 2 ) e. CC )
19 13 18 addcomd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x -h y ) ) ^ 2 ) ) = ( ( ( normh ` ( x -h y ) ) ^ 2 ) + ( ( normh ` ( x +h y ) ) ^ 2 ) ) )
20 8 19 eqtr3d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( ( ( normh ` ( x -h y ) ) ^ 2 ) + ( ( normh ` ( x +h y ) ) ^ 2 ) ) )
21 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
22 21 recnd 
 |-  ( x e. ~H -> ( normh ` x ) e. CC )
23 22 sqcld 
 |-  ( x e. ~H -> ( ( normh ` x ) ^ 2 ) e. CC )
24 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
25 24 recnd 
 |-  ( y e. ~H -> ( normh ` y ) e. CC )
26 25 sqcld 
 |-  ( y e. ~H -> ( ( normh ` y ) ^ 2 ) e. CC )
27 2cn 
 |-  2 e. CC
28 adddi 
 |-  ( ( 2 e. CC /\ ( ( normh ` x ) ^ 2 ) e. CC /\ ( ( normh ` y ) ^ 2 ) e. CC ) -> ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) = ( ( 2 x. ( ( normh ` x ) ^ 2 ) ) + ( 2 x. ( ( normh ` y ) ^ 2 ) ) ) )
29 27 28 mp3an1 
 |-  ( ( ( ( normh ` x ) ^ 2 ) e. CC /\ ( ( normh ` y ) ^ 2 ) e. CC ) -> ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) = ( ( 2 x. ( ( normh ` x ) ^ 2 ) ) + ( 2 x. ( ( normh ` y ) ^ 2 ) ) ) )
30 23 26 29 syl2an 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) = ( ( 2 x. ( ( normh ` x ) ^ 2 ) ) + ( 2 x. ( ( normh ` y ) ^ 2 ) ) ) )
31 4 20 30 3eqtr4d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) )
32 31 rgen2 
 |-  A. x e. ~H A. y e. ~H ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) )
33 hilablo 
 |-  +h e. AbelOp
34 33 elexi 
 |-  +h e. _V
35 hvmulex 
 |-  .h e. _V
36 normf 
 |-  normh : ~H --> RR
37 ax-hilex 
 |-  ~H e. _V
38 fex 
 |-  ( ( normh : ~H --> RR /\ ~H e. _V ) -> normh e. _V )
39 36 37 38 mp2an 
 |-  normh e. _V
40 1 eleq1i 
 |-  ( U e. CPreHilOLD <-> <. <. +h , .h >. , normh >. e. CPreHilOLD )
41 ablogrpo 
 |-  ( +h e. AbelOp -> +h e. GrpOp )
42 33 41 ax-mp 
 |-  +h e. GrpOp
43 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
44 43 fdmi 
 |-  dom +h = ( ~H X. ~H )
45 42 44 grporn 
 |-  ~H = ran +h
46 45 isphg 
 |-  ( ( +h e. _V /\ .h e. _V /\ normh e. _V ) -> ( <. <. +h , .h >. , normh >. e. CPreHilOLD <-> ( <. <. +h , .h >. , normh >. e. NrmCVec /\ A. x e. ~H A. y e. ~H ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) ) ) )
47 40 46 bitrid 
 |-  ( ( +h e. _V /\ .h e. _V /\ normh e. _V ) -> ( U e. CPreHilOLD <-> ( <. <. +h , .h >. , normh >. e. NrmCVec /\ A. x e. ~H A. y e. ~H ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) ) ) )
48 34 35 39 47 mp3an 
 |-  ( U e. CPreHilOLD <-> ( <. <. +h , .h >. , normh >. e. NrmCVec /\ A. x e. ~H A. y e. ~H ( ( ( normh ` ( x +h y ) ) ^ 2 ) + ( ( normh ` ( x +h ( -u 1 .h y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( normh ` x ) ^ 2 ) + ( ( normh ` y ) ^ 2 ) ) ) ) )
49 3 32 48 mpbir2an 
 |-  U e. CPreHilOLD