Metamath Proof Explorer

Theorem pythi

Description: The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space U . The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in Kreyszig p. 135. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses pyth.1 
|- X = ( BaseSet ` U )
pyth.2 
|- G = ( +v ` U )
pyth.6 
|- N = ( normCV ` U )
pyth.7 
|- P = ( .iOLD ` U )
pythi.u 
|- U e. CPreHilOLD
pythi.a 
|- A e. X
pythi.b 
|- B e. X
Assertion pythi 
|- ( ( A P B ) = 0 -> ( ( N ` ( A G B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pyth.1 
 |-  X = ( BaseSet ` U )
2 pyth.2 
 |-  G = ( +v ` U )
3 pyth.6 
 |-  N = ( normCV ` U )
4 pyth.7 
 |-  P = ( .iOLD ` U )
5 pythi.u 
 |-  U e. CPreHilOLD
6 pythi.a 
 |-  A e. X
7 pythi.b 
 |-  B e. X
8 1 2 4 5 6 7 6 7 ip2dii 
 |-  ( ( A G B ) P ( A G B ) ) = ( ( ( A P A ) + ( B P B ) ) + ( ( A P B ) + ( B P A ) ) )
9 id 
 |-  ( ( A P B ) = 0 -> ( A P B ) = 0 )
10 5 phnvi 
 |-  U e. NrmCVec
11 1 4 diporthcom 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) = 0 <-> ( B P A ) = 0 ) )
12 10 6 7 11 mp3an 
 |-  ( ( A P B ) = 0 <-> ( B P A ) = 0 )
13 12 biimpi 
 |-  ( ( A P B ) = 0 -> ( B P A ) = 0 )
14 9 13 oveq12d 
 |-  ( ( A P B ) = 0 -> ( ( A P B ) + ( B P A ) ) = ( 0 + 0 ) )
15 00id 
 |-  ( 0 + 0 ) = 0
16 14 15 eqtrdi 
 |-  ( ( A P B ) = 0 -> ( ( A P B ) + ( B P A ) ) = 0 )
17 16 oveq2d 
 |-  ( ( A P B ) = 0 -> ( ( ( A P A ) + ( B P B ) ) + ( ( A P B ) + ( B P A ) ) ) = ( ( ( A P A ) + ( B P B ) ) + 0 ) )
18 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ A e. X ) -> ( A P A ) e. CC )
19 10 6 6 18 mp3an 
 |-  ( A P A ) e. CC
20 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ B e. X ) -> ( B P B ) e. CC )
21 10 7 7 20 mp3an 
 |-  ( B P B ) e. CC
22 19 21 addcli 
 |-  ( ( A P A ) + ( B P B ) ) e. CC
23 22 addid1i 
 |-  ( ( ( A P A ) + ( B P B ) ) + 0 ) = ( ( A P A ) + ( B P B ) )
24 17 23 eqtrdi 
 |-  ( ( A P B ) = 0 -> ( ( ( A P A ) + ( B P B ) ) + ( ( A P B ) + ( B P A ) ) ) = ( ( A P A ) + ( B P B ) ) )
25 8 24 syl5eq 
 |-  ( ( A P B ) = 0 -> ( ( A G B ) P ( A G B ) ) = ( ( A P A ) + ( B P B ) ) )
26 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
27 10 6 7 26 mp3an 
 |-  ( A G B ) e. X
28 1 3 4 ipidsq 
 |-  ( ( U e. NrmCVec /\ ( A G B ) e. X ) -> ( ( A G B ) P ( A G B ) ) = ( ( N ` ( A G B ) ) ^ 2 ) )
29 10 27 28 mp2an 
 |-  ( ( A G B ) P ( A G B ) ) = ( ( N ` ( A G B ) ) ^ 2 )
30 1 3 4 ipidsq 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )
31 10 6 30 mp2an 
 |-  ( A P A ) = ( ( N ` A ) ^ 2 )
32 1 3 4 ipidsq 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( B P B ) = ( ( N ` B ) ^ 2 ) )
33 10 7 32 mp2an 
 |-  ( B P B ) = ( ( N ` B ) ^ 2 )
34 31 33 oveq12i 
 |-  ( ( A P A ) + ( B P B ) ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) )
35 25 29 34 3eqtr3g 
 |-  ( ( A P B ) = 0 -> ( ( N ` ( A G B ) ) ^ 2 ) = ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )