# 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}\in ℋ$
normpar2.2 ${⊢}{B}\in ℋ$
normpar2.3 ${⊢}{C}\in ℋ$
Assertion normpar2i ${⊢}{{norm}_{ℎ}\left({A}{-}_{ℎ}{B}\right)}^{2}=2{{norm}_{ℎ}\left({A}{-}_{ℎ}{C}\right)}^{2}+2{{norm}_{ℎ}\left({B}{-}_{ℎ}{C}\right)}^{2}-{{norm}_{ℎ}\left(\left({A}{+}_{ℎ}{B}\right){-}_{ℎ}\left(2{\cdot }_{ℎ}{C}\right)\right)}^{2}$

### Proof

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