Metamath Proof Explorer

Theorem phpar2

Description: The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007) (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 phpar2 
|- ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 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 1 2 3 4 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 ) ) ) ) )
6 5 simprbi 
 |-  ( 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 ) ) ) )
7 6 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 M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) )
8 fvoveq1 
 |-  ( x = A -> ( N ` ( x G y ) ) = ( N ` ( A G y ) ) )
9 8 oveq1d 
 |-  ( x = A -> ( ( N ` ( x G y ) ) ^ 2 ) = ( ( N ` ( A G y ) ) ^ 2 ) )
10 fvoveq1 
 |-  ( x = A -> ( N ` ( x M y ) ) = ( N ` ( A M y ) ) )
11 10 oveq1d 
 |-  ( x = A -> ( ( N ` ( x M y ) ) ^ 2 ) = ( ( N ` ( A M y ) ) ^ 2 ) )
12 9 11 oveq12d 
 |-  ( x = A -> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A M y ) ) ^ 2 ) ) )
13 fveq2 
 |-  ( x = A -> ( N ` x ) = ( N ` A ) )
14 13 oveq1d 
 |-  ( x = A -> ( ( N ` x ) ^ 2 ) = ( ( N ` A ) ^ 2 ) )
15 14 oveq1d 
 |-  ( x = A -> ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) )
16 15 oveq2d 
 |-  ( x = A -> ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) )
17 12 16 eqeq12d 
 |-  ( x = A -> ( ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) )
18 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
19 18 fveq2d 
 |-  ( y = B -> ( N ` ( A G y ) ) = ( N ` ( A G B ) ) )
20 19 oveq1d 
 |-  ( y = B -> ( ( N ` ( A G y ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
21 oveq2 
 |-  ( y = B -> ( A M y ) = ( A M B ) )
22 21 fveq2d 
 |-  ( y = B -> ( N ` ( A M y ) ) = ( N ` ( A M B ) ) )
23 22 oveq1d 
 |-  ( y = B -> ( ( N ` ( A M y ) ) ^ 2 ) = ( ( N ` ( A M B ) ) ^ 2 ) )
24 20 23 oveq12d 
 |-  ( y = B -> ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A M y ) ) ^ 2 ) ) = ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) )
25 fveq2 
 |-  ( y = B -> ( N ` y ) = ( N ` B ) )
26 25 oveq1d 
 |-  ( y = B -> ( ( N ` y ) ^ 2 ) = ( ( N ` B ) ^ 2 ) )
27 26 oveq2d 
 |-  ( y = B -> ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )
28 27 oveq2d 
 |-  ( y = B -> ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
29 24 28 eqeq12d 
 |-  ( y = B -> ( ( ( ( N ` ( A G y ) ) ^ 2 ) + ( ( N ` ( A M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
30 17 29 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( 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 ) ) ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
31 30 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 M y ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) ) )
32 7 31 mpd 
 |-  ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A M B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )