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. This is Metamath 100 proof #4. (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 = norm CV U
pyth.7 P = 𝑖OLD U
pythi.u U CPreHil OLD
pythi.a A X
pythi.b B 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 = norm CV U
4 pyth.7 P = 𝑖OLD U
5 pythi.u U CPreHil OLD
6 pythi.a A X
7 pythi.b B 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 NrmCVec
11 1 4 diporthcom U NrmCVec A X B 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 syl6eq 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 NrmCVec A X A X A P A
19 10 6 6 18 mp3an A P A
20 1 4 dipcl U NrmCVec B X B X B P B
21 10 7 7 20 mp3an B P B
22 19 21 addcli A P A + B P B
23 22 addid1i A P A + B P B + 0 = A P A + B P B
24 17 23 syl6eq 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 NrmCVec A X B X A G B X
27 10 6 7 26 mp3an A G B X
28 1 3 4 ipidsq U NrmCVec A G B 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 NrmCVec A X A P A = N A 2
31 10 6 30 mp2an A P A = N A 2
32 1 3 4 ipidsq U NrmCVec B 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