This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem normpari

Description: Parallelogram law for norms. Remark 3.4(B) of Beran p. 98. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normpar.1 
|- A e. ~H
normpar.2 
|- B e. ~H
Assertion normpari 
|- ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 normpar.1 
 |-  A e. ~H
2 normpar.2 
 |-  B e. ~H
3 1 2 hvsubcli 
 |-  ( A -h B ) e. ~H
4 3 normsqi 
 |-  ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( A -h B ) .ih ( A -h B ) )
5 1 2 hvaddcli 
 |-  ( A +h B ) e. ~H
6 5 normsqi 
 |-  ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( A +h B ) .ih ( A +h B ) )
7 4 6 oveq12i 
 |-  ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )
8 1 normsqi 
 |-  ( ( normh ` A ) ^ 2 ) = ( A .ih A )
9 8 oveq2i 
 |-  ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( 2 x. ( A .ih A ) )
10 1 1 hicli 
 |-  ( A .ih A ) e. CC
11 10 2timesi 
 |-  ( 2 x. ( A .ih A ) ) = ( ( A .ih A ) + ( A .ih A ) )
12 9 11 eqtri 
 |-  ( 2 x. ( ( normh ` A ) ^ 2 ) ) = ( ( A .ih A ) + ( A .ih A ) )
13 2 normsqi 
 |-  ( ( normh ` B ) ^ 2 ) = ( B .ih B )
14 13 oveq2i 
 |-  ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( 2 x. ( B .ih B ) )
15 2 2 hicli 
 |-  ( B .ih B ) e. CC
16 15 2timesi 
 |-  ( 2 x. ( B .ih B ) ) = ( ( B .ih B ) + ( B .ih B ) )
17 14 16 eqtri 
 |-  ( 2 x. ( ( normh ` B ) ^ 2 ) ) = ( ( B .ih B ) + ( B .ih B ) )
18 12 17 oveq12i 
 |-  ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
19 1 2 1 2 normlem9 
 |-  ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )
20 10 15 addcli 
 |-  ( ( A .ih A ) + ( B .ih B ) ) e. CC
21 1 2 hicli 
 |-  ( A .ih B ) e. CC
22 2 1 hicli 
 |-  ( B .ih A ) e. CC
23 21 22 addcli 
 |-  ( ( A .ih B ) + ( B .ih A ) ) e. CC
24 20 23 negsubi 
 |-  ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) - ( ( A .ih B ) + ( B .ih A ) ) )
25 19 24 eqtr4i 
 |-  ( ( A -h B ) .ih ( A -h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) )
26 1 2 1 2 normlem8 
 |-  ( ( A +h B ) .ih ( A +h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) )
27 25 26 oveq12i 
 |-  ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) + ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) )
28 23 negcli 
 |-  -u ( ( A .ih B ) + ( B .ih A ) ) e. CC
29 20 28 20 23 add42i 
 |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) + ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) )
30 23 negidi 
 |-  ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) = 0
31 30 oveq2i 
 |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + 0 )
32 20 20 addcli 
 |-  ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) e. CC
33 32 addridi 
 |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + 0 ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) )
34 10 15 10 15 add4i 
 |-  ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
35 31 33 34 3eqtri 
 |-  ( ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih A ) + ( B .ih B ) ) ) + ( ( ( A .ih B ) + ( B .ih A ) ) + -u ( ( A .ih B ) + ( B .ih A ) ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
36 27 29 35 3eqtri 
 |-  ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) ) = ( ( ( A .ih A ) + ( A .ih A ) ) + ( ( B .ih B ) + ( B .ih B ) ) )
37 18 36 eqtr4i 
 |-  ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) + ( ( A +h B ) .ih ( A +h B ) ) )
38 7 37 eqtr4i 
 |-  ( ( ( normh ` ( A -h B ) ) ^ 2 ) + ( ( normh ` ( A +h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` A ) ^ 2 ) ) + ( 2 x. ( ( normh ` B ) ^ 2 ) ) )