Metamath Proof Explorer

Theorem isphg

Description: The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is G , the scalar product is S , and the norm is N . An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis isphg.1 
|- X = ran G
Assertion isphg 
|- ( ( G e. A /\ S e. B /\ N e. C ) -> ( <. <. G , S >. , N >. e. CPreHilOLD <-> ( <. <. G , S >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isphg.1 
 |-  X = ran G
2 df-ph 
 |-  CPreHilOLD = ( NrmCVec i^i { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } )
3 2 elin2 
 |-  ( <. <. G , S >. , N >. e. CPreHilOLD <-> ( <. <. G , S >. , N >. e. NrmCVec /\ <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } ) )
4 rneq 
 |-  ( g = G -> ran g = ran G )
5 4 1 eqtr4di 
 |-  ( g = G -> ran g = X )
6 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
7 6 fveq2d 
 |-  ( g = G -> ( n ` ( x g y ) ) = ( n ` ( x G y ) ) )
8 7 oveq1d 
 |-  ( g = G -> ( ( n ` ( x g y ) ) ^ 2 ) = ( ( n ` ( x G y ) ) ^ 2 ) )
9 oveq 
 |-  ( g = G -> ( x g ( -u 1 s y ) ) = ( x G ( -u 1 s y ) ) )
10 9 fveq2d 
 |-  ( g = G -> ( n ` ( x g ( -u 1 s y ) ) ) = ( n ` ( x G ( -u 1 s y ) ) ) )
11 10 oveq1d 
 |-  ( g = G -> ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) = ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) )
12 8 11 oveq12d 
 |-  ( g = G -> ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) )
13 12 eqeq1d 
 |-  ( g = G -> ( ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) )
14 5 13 raleqbidv 
 |-  ( g = G -> ( A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) )
15 5 14 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) )
16 oveq 
 |-  ( s = S -> ( -u 1 s y ) = ( -u 1 S y ) )
17 16 oveq2d 
 |-  ( s = S -> ( x G ( -u 1 s y ) ) = ( x G ( -u 1 S y ) ) )
18 17 fveq2d 
 |-  ( s = S -> ( n ` ( x G ( -u 1 s y ) ) ) = ( n ` ( x G ( -u 1 S y ) ) ) )
19 18 oveq1d 
 |-  ( s = S -> ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) = ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) )
20 19 oveq2d 
 |-  ( s = S -> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) )
21 20 eqeq1d 
 |-  ( s = S -> ( ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) )
22 21 2ralbidv 
 |-  ( s = S -> ( A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) )
23 fveq1 
 |-  ( n = N -> ( n ` ( x G y ) ) = ( N ` ( x G y ) ) )
24 23 oveq1d 
 |-  ( n = N -> ( ( n ` ( x G y ) ) ^ 2 ) = ( ( N ` ( x G y ) ) ^ 2 ) )
25 fveq1 
 |-  ( n = N -> ( n ` ( x G ( -u 1 S y ) ) ) = ( N ` ( x G ( -u 1 S y ) ) ) )
26 25 oveq1d 
 |-  ( n = N -> ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) = ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) )
27 24 26 oveq12d 
 |-  ( n = N -> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) )
28 fveq1 
 |-  ( n = N -> ( n ` x ) = ( N ` x ) )
29 28 oveq1d 
 |-  ( n = N -> ( ( n ` x ) ^ 2 ) = ( ( N ` x ) ^ 2 ) )
30 fveq1 
 |-  ( n = N -> ( n ` y ) = ( N ` y ) )
31 30 oveq1d 
 |-  ( n = N -> ( ( n ` y ) ^ 2 ) = ( ( N ` y ) ^ 2 ) )
32 29 31 oveq12d 
 |-  ( n = N -> ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) = ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) )
33 32 oveq2d 
 |-  ( n = N -> ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) )
34 27 33 eqeq12d 
 |-  ( n = N -> ( ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
35 34 2ralbidv 
 |-  ( n = N -> ( A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
36 15 22 35 eloprabg 
 |-  ( ( G e. A /\ S e. B /\ N e. C ) -> ( <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } <-> A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
37 36 anbi2d 
 |-  ( ( G e. A /\ S e. B /\ N e. C ) -> ( ( <. <. G , S >. , N >. e. NrmCVec /\ <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } ) <-> ( <. <. G , S >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
38 3 37 bitrid 
 |-  ( ( G e. A /\ S e. B /\ N e. C ) -> ( <. <. G , S >. , N >. e. CPreHilOLD <-> ( <. <. G , S >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )