Metamath Proof Explorer

Theorem phpar

Description: The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses phpar.1 
|- X = ( BaseSet ` U )
phpar.2 
|- G = ( +v ` U )
phpar.4 
|- S = ( .sOLD ` U )
phpar.6 
|- N = ( normCV ` U )
Assertion phpar 
|- ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 phpar.1 
 |-  X = ( BaseSet ` U )
2 phpar.2 
 |-  G = ( +v ` U )
3 phpar.4 
 |-  S = ( .sOLD ` U )
4 phpar.6 
 |-  N = ( normCV ` U )
5 2 fvexi 
 |-  G e. _V
6 3 fvexi 
 |-  S e. _V
7 4 fvexi 
 |-  N e. _V
8 5 6 7 3pm3.2i 
 |-  ( G e. _V /\ S e. _V /\ N e. _V )
9 2 3 4 phop 
 |-  ( U e. CPreHilOLD -> U = <. <. G , S >. , N >. )
10 9 eleq1d 
 |-  ( U e. CPreHilOLD -> ( U e. CPreHilOLD <-> <. <. G , S >. , N >. e. CPreHilOLD ) )
11 10 ibi 
 |-  ( U e. CPreHilOLD -> <. <. G , S >. , N >. e. CPreHilOLD )
12 1 2 bafval 
 |-  X = ran G
13 12 isphg 
 |-  ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. 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 ) ) ) ) ) )
14 13 simplbda 
 |-  ( ( ( G e. _V /\ S e. _V /\ N e. _V ) /\ <. <. G , S >. , N >. e. CPreHilOLD ) -> 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 ) ) ) )
15 8 11 14 sylancr 
 |-  ( U e. CPreHilOLD -> 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 15 3ad2ant1 
 |-  ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> 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 ) ) ) )
17 fvoveq1 
 |-  ( x = A -> ( N ` ( x G y ) ) = ( N ` ( A G y ) ) )
18 17 oveq1d 
 |-  ( x = A -> ( ( N ` ( x G y ) ) ^ 2 ) = ( ( N ` ( A G y ) ) ^ 2 ) )
19 fvoveq1 
 |-  ( x = A -> ( N ` ( x G ( -u 1 S y ) ) ) = ( N ` ( A G ( -u 1 S y ) ) ) )
20 19 oveq1d 
 |-  ( x = A -> ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) = ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) )
21 18 20 oveq12d 
 |-  ( x = A -> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) ) )
22 fveq2 
 |-  ( x = A -> ( N ` x ) = ( N ` A ) )
23 22 oveq1d 
 |-  ( x = A -> ( ( N ` x ) ^ 2 ) = ( ( N ` A ) ^ 2 ) )
24 23 oveq1d 
 |-  ( x = A -> ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) )
25 24 oveq2d 
 |-  ( x = A -> ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) )
26 21 25 eqeq12d 
 |-  ( x = A -> ( ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
27 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
28 27 fveq2d 
 |-  ( y = B -> ( N ` ( A G y ) ) = ( N ` ( A G B ) ) )
29 28 oveq1d 
 |-  ( y = B -> ( ( N ` ( A G y ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
30 oveq2 
 |-  ( y = B -> ( -u 1 S y ) = ( -u 1 S B ) )
31 30 oveq2d 
 |-  ( y = B -> ( A G ( -u 1 S y ) ) = ( A G ( -u 1 S B ) ) )
32 31 fveq2d 
 |-  ( y = B -> ( N ` ( A G ( -u 1 S y ) ) ) = ( N ` ( A G ( -u 1 S B ) ) ) )
33 32 oveq1d 
 |-  ( y = B -> ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) = ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) )
34 29 33 oveq12d 
 |-  ( y = B -> ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) ) = ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
35 fveq2 
 |-  ( y = B -> ( N ` y ) = ( N ` B ) )
36 35 oveq1d 
 |-  ( y = B -> ( ( N ` y ) ^ 2 ) = ( ( N ` B ) ^ 2 ) )
37 36 oveq2d 
 |-  ( y = B -> ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )
38 37 oveq2d 
 |-  ( y = B -> ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
39 34 38 eqeq12d 
 |-  ( y = B -> ( ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
40 26 39 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( 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 ) ) ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
41 40 3adant1 
 |-  ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( 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 ) ) ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
42 16 41 mpd 
 |-  ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )