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 addridi 
 |-  ( ( ( 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 ) ) )