Metamath Proof Explorer


Theorem normpythi

Description: Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of Beran p. 98. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normsub.1 A
normsub.2 B
Assertion normpythi AihB=0normA+B2=normA2+normB2

Proof

Step Hyp Ref Expression
1 normsub.1 A
2 normsub.2 B
3 1 2 1 2 normlem8 A+BihA+B=AihA+BihB+AihB+BihA
4 id AihB=0AihB=0
5 orthcom ABAihB=0BihA=0
6 1 2 5 mp2an AihB=0BihA=0
7 6 biimpi AihB=0BihA=0
8 4 7 oveq12d AihB=0AihB+BihA=0+0
9 00id 0+0=0
10 8 9 eqtrdi AihB=0AihB+BihA=0
11 10 oveq2d AihB=0AihA+BihB+AihB+BihA=AihA+BihB+0
12 1 1 hicli AihA
13 2 2 hicli BihB
14 12 13 addcli AihA+BihB
15 14 addid1i AihA+BihB+0=AihA+BihB
16 11 15 eqtrdi AihB=0AihA+BihB+AihB+BihA=AihA+BihB
17 3 16 eqtrid AihB=0A+BihA+B=AihA+BihB
18 1 2 hvaddcli A+B
19 18 normsqi normA+B2=A+BihA+B
20 1 normsqi normA2=AihA
21 2 normsqi normB2=BihB
22 20 21 oveq12i normA2+normB2=AihA+BihB
23 17 19 22 3eqtr4g AihB=0normA+B2=normA2+normB2