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 syl5bb
 |-  ( ( +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