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 ⊢ 𝐴 ∈ ℋ
normpar2.2 ⊢ 𝐵 ∈ ℋ
normpar2.3 ⊢ 𝐶 ∈ ℋ
Assertion normpar2i ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) = ( ( ( 2 · ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ↑ 2 ) ) ) − ( ( normℎ ‘ ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 2 ·ℎ 𝐶 ) ) ) ↑ 2 ) )

Proof

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