Metamath Proof Explorer

Theorem normpar2i

Description: Corollary of parallelogram law for norms. Part of Lemma 3.6 of Beran p. 100. (Contributed by NM, 5-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normpar2.1 
|- A e. ~H
normpar2.2 
|- B e. ~H
normpar2.3 
|- C e. ~H
Assertion normpar2i 
|- ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) - ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 normpar2.1 
 |-  A e. ~H
2 normpar2.2 
 |-  B e. ~H
3 normpar2.3 
 |-  C e. ~H
4 1 2 hvaddcli 
 |-  ( A +h B ) e. ~H
5 2cn 
 |-  2 e. CC
6 5 3 hvmulcli 
 |-  ( 2 .h C ) e. ~H
7 4 6 hvsubcli 
 |-  ( ( A +h B ) -h ( 2 .h C ) ) e. ~H
8 7 normcli 
 |-  ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) e. RR
9 8 resqcli 
 |-  ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) e. RR
10 9 recni 
 |-  ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) e. CC
11 1 2 hvsubcli 
 |-  ( A -h B ) e. ~H
12 11 normcli 
 |-  ( normh ` ( A -h B ) ) e. RR
13 12 resqcli 
 |-  ( ( normh ` ( A -h B ) ) ^ 2 ) e. RR
14 13 recni 
 |-  ( ( normh ` ( A -h B ) ) ^ 2 ) e. CC
15 4cn 
 |-  4 e. CC
16 1 3 hvsubcli 
 |-  ( A -h C ) e. ~H
17 16 normcli 
 |-  ( normh ` ( A -h C ) ) e. RR
18 17 resqcli 
 |-  ( ( normh ` ( A -h C ) ) ^ 2 ) e. RR
19 18 recni 
 |-  ( ( normh ` ( A -h C ) ) ^ 2 ) e. CC
20 15 19 mulcli 
 |-  ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) e. CC
21 2 3 hvsubcli 
 |-  ( B -h C ) e. ~H
22 21 normcli 
 |-  ( normh ` ( B -h C ) ) e. RR
23 22 resqcli 
 |-  ( ( normh ` ( B -h C ) ) ^ 2 ) e. RR
24 23 recni 
 |-  ( ( normh ` ( B -h C ) ) ^ 2 ) e. CC
25 15 24 mulcli 
 |-  ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) e. CC
26 2ne0 
 |-  2 =/= 0
27 20 25 5 26 divdiri 
 |-  ( ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) / 2 ) = ( ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) / 2 ) + ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) / 2 ) )
28 20 25 addcomi 
 |-  ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) = ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) )
29 neg1cn 
 |-  -u 1 e. CC
30 29 6 hvmulcli 
 |-  ( -u 1 .h ( 2 .h C ) ) e. ~H
31 29 11 hvmulcli 
 |-  ( -u 1 .h ( A -h B ) ) e. ~H
32 4 30 31 hvadd32i 
 |-  ( ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) ) +h ( -u 1 .h ( A -h B ) ) ) = ( ( ( A +h B ) +h ( -u 1 .h ( A -h B ) ) ) +h ( -u 1 .h ( 2 .h C ) ) )
33 4 6 hvsubvali 
 |-  ( ( A +h B ) -h ( 2 .h C ) ) = ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) )
34 33 oveq1i 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( -u 1 .h ( A -h B ) ) ) = ( ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) ) +h ( -u 1 .h ( A -h B ) ) )
35 5 2 hvmulcli 
 |-  ( 2 .h B ) e. ~H
36 35 6 hvsubvali 
 |-  ( ( 2 .h B ) -h ( 2 .h C ) ) = ( ( 2 .h B ) +h ( -u 1 .h ( 2 .h C ) ) )
37 1 2 hvcomi 
 |-  ( A +h B ) = ( B +h A )
38 1 2 hvnegdii 
 |-  ( -u 1 .h ( A -h B ) ) = ( B -h A )
39 37 38 oveq12i 
 |-  ( ( A +h B ) +h ( -u 1 .h ( A -h B ) ) ) = ( ( B +h A ) +h ( B -h A ) )
40 2 1 hvsubcan2i 
 |-  ( ( B +h A ) +h ( B -h A ) ) = ( 2 .h B )
41 39 40 eqtri 
 |-  ( ( A +h B ) +h ( -u 1 .h ( A -h B ) ) ) = ( 2 .h B )
42 41 oveq1i 
 |-  ( ( ( A +h B ) +h ( -u 1 .h ( A -h B ) ) ) +h ( -u 1 .h ( 2 .h C ) ) ) = ( ( 2 .h B ) +h ( -u 1 .h ( 2 .h C ) ) )
43 36 42 eqtr4i 
 |-  ( ( 2 .h B ) -h ( 2 .h C ) ) = ( ( ( A +h B ) +h ( -u 1 .h ( A -h B ) ) ) +h ( -u 1 .h ( 2 .h C ) ) )
44 32 34 43 3eqtr4i 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( -u 1 .h ( A -h B ) ) ) = ( ( 2 .h B ) -h ( 2 .h C ) )
45 7 11 hvsubvali 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) = ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( -u 1 .h ( A -h B ) ) )
46 5 2 3 hvsubdistr1i 
 |-  ( 2 .h ( B -h C ) ) = ( ( 2 .h B ) -h ( 2 .h C ) )
47 44 45 46 3eqtr4i 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) = ( 2 .h ( B -h C ) )
48 47 fveq2i 
 |-  ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) = ( normh ` ( 2 .h ( B -h C ) ) )
49 5 21 norm-iii-i 
 |-  ( normh ` ( 2 .h ( B -h C ) ) ) = ( ( abs ` 2 ) x. ( normh ` ( B -h C ) ) )
50 0le2 
 |-  0 <_ 2
51 2re 
 |-  2 e. RR
52 51 absidi 
 |-  ( 0 <_ 2 -> ( abs ` 2 ) = 2 )
53 50 52 ax-mp 
 |-  ( abs ` 2 ) = 2
54 53 oveq1i 
 |-  ( ( abs ` 2 ) x. ( normh ` ( B -h C ) ) ) = ( 2 x. ( normh ` ( B -h C ) ) )
55 48 49 54 3eqtri 
 |-  ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) = ( 2 x. ( normh ` ( B -h C ) ) )
56 55 oveq1i 
 |-  ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) ^ 2 ) = ( ( 2 x. ( normh ` ( B -h C ) ) ) ^ 2 )
57 22 recni 
 |-  ( normh ` ( B -h C ) ) e. CC
58 5 57 sqmuli 
 |-  ( ( 2 x. ( normh ` ( B -h C ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
59 sq2 
 |-  ( 2 ^ 2 ) = 4
60 59 oveq1i 
 |-  ( ( 2 ^ 2 ) x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) = ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
61 56 58 60 3eqtri 
 |-  ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) ^ 2 ) = ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
62 1 2 hvsubcan2i 
 |-  ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )
63 62 oveq1i 
 |-  ( ( ( A +h B ) +h ( A -h B ) ) +h ( -u 1 .h ( 2 .h C ) ) ) = ( ( 2 .h A ) +h ( -u 1 .h ( 2 .h C ) ) )
64 4 30 11 hvadd32i 
 |-  ( ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) ) +h ( A -h B ) ) = ( ( ( A +h B ) +h ( A -h B ) ) +h ( -u 1 .h ( 2 .h C ) ) )
65 5 1 hvmulcli 
 |-  ( 2 .h A ) e. ~H
66 65 6 hvsubvali 
 |-  ( ( 2 .h A ) -h ( 2 .h C ) ) = ( ( 2 .h A ) +h ( -u 1 .h ( 2 .h C ) ) )
67 63 64 66 3eqtr4i 
 |-  ( ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) ) +h ( A -h B ) ) = ( ( 2 .h A ) -h ( 2 .h C ) )
68 33 oveq1i 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) = ( ( ( A +h B ) +h ( -u 1 .h ( 2 .h C ) ) ) +h ( A -h B ) )
69 5 1 3 hvsubdistr1i 
 |-  ( 2 .h ( A -h C ) ) = ( ( 2 .h A ) -h ( 2 .h C ) )
70 67 68 69 3eqtr4i 
 |-  ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) = ( 2 .h ( A -h C ) )
71 70 fveq2i 
 |-  ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) = ( normh ` ( 2 .h ( A -h C ) ) )
72 5 16 norm-iii-i 
 |-  ( normh ` ( 2 .h ( A -h C ) ) ) = ( ( abs ` 2 ) x. ( normh ` ( A -h C ) ) )
73 53 oveq1i 
 |-  ( ( abs ` 2 ) x. ( normh ` ( A -h C ) ) ) = ( 2 x. ( normh ` ( A -h C ) ) )
74 71 72 73 3eqtri 
 |-  ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) = ( 2 x. ( normh ` ( A -h C ) ) )
75 74 oveq1i 
 |-  ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) ^ 2 ) = ( ( 2 x. ( normh ` ( A -h C ) ) ) ^ 2 )
76 17 recni 
 |-  ( normh ` ( A -h C ) ) e. CC
77 5 76 sqmuli 
 |-  ( ( 2 x. ( normh ` ( A -h C ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
78 59 oveq1i 
 |-  ( ( 2 ^ 2 ) x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) = ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
79 75 77 78 3eqtri 
 |-  ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) ^ 2 ) = ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
80 61 79 oveq12i 
 |-  ( ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) ^ 2 ) + ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) ^ 2 ) ) = ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) )
81 28 80 eqtr4i 
 |-  ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) = ( ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) ^ 2 ) + ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) ^ 2 ) )
82 7 11 normpari 
 |-  ( ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) -h ( A -h B ) ) ) ^ 2 ) + ( ( normh ` ( ( ( A +h B ) -h ( 2 .h C ) ) +h ( A -h B ) ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) )
83 81 82 eqtri 
 |-  ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) = ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) )
84 83 oveq1i 
 |-  ( ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) / 2 ) = ( ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) ) / 2 )
85 5 10 mulcli 
 |-  ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) e. CC
86 5 14 mulcli 
 |-  ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) e. CC
87 85 86 5 26 divdiri 
 |-  ( ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) ) / 2 ) = ( ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) / 2 ) + ( ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) / 2 ) )
88 10 5 26 divcan3i 
 |-  ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) / 2 ) = ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 )
89 14 5 26 divcan3i 
 |-  ( ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) / 2 ) = ( ( normh ` ( A -h B ) ) ^ 2 )
90 88 89 oveq12i 
 |-  ( ( ( 2 x. ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) ) / 2 ) + ( ( 2 x. ( ( normh ` ( A -h B ) ) ^ 2 ) ) / 2 ) ) = ( ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) + ( ( normh ` ( A -h B ) ) ^ 2 ) )
91 84 87 90 3eqtri 
 |-  ( ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) / 2 ) = ( ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) + ( ( normh ` ( A -h B ) ) ^ 2 ) )
92 15 19 5 26 div23i 
 |-  ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) / 2 ) = ( ( 4 / 2 ) x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
93 4d2e2 
 |-  ( 4 / 2 ) = 2
94 93 oveq1i 
 |-  ( ( 4 / 2 ) x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) = ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
95 92 94 eqtri 
 |-  ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) / 2 ) = ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) )
96 15 24 5 26 div23i 
 |-  ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) / 2 ) = ( ( 4 / 2 ) x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
97 93 oveq1i 
 |-  ( ( 4 / 2 ) x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) = ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
98 96 97 eqtri 
 |-  ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) / 2 ) = ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) )
99 95 98 oveq12i 
 |-  ( ( ( 4 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) / 2 ) + ( ( 4 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) / 2 ) ) = ( ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) )
100 27 91 99 3eqtr3i 
 |-  ( ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) + ( ( normh ` ( A -h B ) ) ^ 2 ) ) = ( ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) )
101 10 14 100 mvlladdi 
 |-  ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( ( 2 x. ( ( normh ` ( A -h C ) ) ^ 2 ) ) + ( 2 x. ( ( normh ` ( B -h C ) ) ^ 2 ) ) ) - ( ( normh ` ( ( A +h B ) -h ( 2 .h C ) ) ) ^ 2 ) )