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 e. ~H
normsub.2
|- B e. ~H
Assertion normpythi
|- ( ( A .ih B ) = 0 -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 normsub.1
 |-  A e. ~H
2 normsub.2
 |-  B e. ~H
3 1 2 1 2 normlem8
 |-  ( ( A +h B ) .ih ( A +h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) )
4 id
 |-  ( ( A .ih B ) = 0 -> ( A .ih B ) = 0 )
5 orthcom
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) )
6 1 2 5 mp2an
 |-  ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 )
7 6 biimpi
 |-  ( ( A .ih B ) = 0 -> ( B .ih A ) = 0 )
8 4 7 oveq12d
 |-  ( ( A .ih B ) = 0 -> ( ( A .ih B ) + ( B .ih A ) ) = ( 0 + 0 ) )
9 00id
 |-  ( 0 + 0 ) = 0
10 8 9 eqtrdi
 |-  ( ( A .ih B ) = 0 -> ( ( A .ih B ) + ( B .ih A ) ) = 0 )
11 10 oveq2d
 |-  ( ( A .ih B ) = 0 -> ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + 0 ) )
12 1 1 hicli
 |-  ( A .ih A ) e. CC
13 2 2 hicli
 |-  ( B .ih B ) e. CC
14 12 13 addcli
 |-  ( ( A .ih A ) + ( B .ih B ) ) e. CC
15 14 addid1i
 |-  ( ( ( A .ih A ) + ( B .ih B ) ) + 0 ) = ( ( A .ih A ) + ( B .ih B ) )
16 11 15 eqtrdi
 |-  ( ( A .ih B ) = 0 -> ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( A .ih A ) + ( B .ih B ) ) )
17 3 16 eqtrid
 |-  ( ( A .ih B ) = 0 -> ( ( A +h B ) .ih ( A +h B ) ) = ( ( A .ih A ) + ( B .ih B ) ) )
18 1 2 hvaddcli
 |-  ( A +h B ) e. ~H
19 18 normsqi
 |-  ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( A +h B ) .ih ( A +h B ) )
20 1 normsqi
 |-  ( ( normh ` A ) ^ 2 ) = ( A .ih A )
21 2 normsqi
 |-  ( ( normh ` B ) ^ 2 ) = ( B .ih B )
22 20 21 oveq12i
 |-  ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) = ( ( A .ih A ) + ( B .ih B ) )
23 17 19 22 3eqtr4g
 |-  ( ( A .ih B ) = 0 -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) )