Metamath Proof Explorer

Theorem isph

Description: The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isph.1 
|- X = ( BaseSet ` U )
isph.2 
|- G = ( +v ` U )
isph.3 
|- M = ( -v ` U )
isph.6 
|- N = ( normCV ` U )
Assertion isph 
|- ( U e. CPreHilOLD <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isph.1 
 |-  X = ( BaseSet ` U )
2 isph.2 
 |-  G = ( +v ` U )
3 isph.3 
 |-  M = ( -v ` U )
4 isph.6 
 |-  N = ( normCV ` U )
5 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
6 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
7 2 6 4 nvop 
 |-  ( U e. NrmCVec -> U = <. <. G , ( .sOLD ` U ) >. , N >. )
8 eleq1 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( U e. CPreHilOLD <-> <. <. G , ( .sOLD ` U ) >. , N >. e. CPreHilOLD ) )
9 2 fvexi 
 |-  G e. _V
10 fvex 
 |-  ( .sOLD ` U ) e. _V
11 4 fvexi 
 |-  N e. _V
12 1 2 bafval 
 |-  X = ran G
13 12 isphg 
 |-  ( ( G e. _V /\ ( .sOLD ` U ) e. _V /\ N e. _V ) -> ( <. <. G , ( .sOLD ` U ) >. , N >. e. CPreHilOLD <-> ( <. <. G , ( .sOLD ` U ) >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
14 9 10 11 13 mp3an 
 |-  ( <. <. G , ( .sOLD ` U ) >. , N >. e. CPreHilOLD <-> ( <. <. G , ( .sOLD ` U ) >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
15 1 2 6 3 nvmval 
 |-  ( ( U e. NrmCVec /\ x e. X /\ y e. X ) -> ( x M y ) = ( x G ( -u 1 ( .sOLD ` U ) y ) ) )
16 15 3expa 
 |-  ( ( ( U e. NrmCVec /\ x e. X ) /\ y e. X ) -> ( x M y ) = ( x G ( -u 1 ( .sOLD ` U ) y ) ) )
17 16 fveq2d 
 |-  ( ( ( U e. NrmCVec /\ x e. X ) /\ y e. X ) -> ( N ` ( x M y ) ) = ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) )
18 17 oveq1d 
 |-  ( ( ( U e. NrmCVec /\ x e. X ) /\ y e. X ) -> ( ( N ` ( x M y ) ) ^ 2 ) = ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) )
19 18 oveq2d 
 |-  ( ( ( U e. NrmCVec /\ x e. X ) /\ y e. X ) -> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) )
20 19 eqeq1d 
 |-  ( ( ( U e. NrmCVec /\ x e. X ) /\ y e. X ) -> ( ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
21 20 ralbidva 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
22 21 ralbidva 
 |-  ( U e. NrmCVec -> ( A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M 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 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
23 22 pm5.32i 
 |-  ( ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
24 eleq1 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( U e. NrmCVec <-> <. <. G , ( .sOLD ` U ) >. , N >. e. NrmCVec ) )
25 24 anbi1d 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) <-> ( <. <. G , ( .sOLD ` U ) >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
26 23 25 bitr2id 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( ( <. <. G , ( .sOLD ` U ) >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 ( .sOLD ` U ) y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
27 14 26 bitrid 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( <. <. G , ( .sOLD ` U ) >. , N >. e. CPreHilOLD <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
28 8 27 bitrd 
 |-  ( U = <. <. G , ( .sOLD ` U ) >. , N >. -> ( U e. CPreHilOLD <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
29 7 28 syl 
 |-  ( U e. NrmCVec -> ( U e. CPreHilOLD <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) )
30 29 bianabs 
 |-  ( U e. NrmCVec -> ( U e. CPreHilOLD <-> A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
31 5 30 biadanii 
 |-  ( U e. CPreHilOLD <-> ( U e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )