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 \mathscr{H}$$
	normpar2.2	$$⊢B\in \mathscr{H}$$
	normpar2.3	$$⊢C\in \mathscr{H}$$
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 \mathscr{H}$$
2		normpar2.2	$$⊢B\in \mathscr{H}$$
3		normpar2.3	$$⊢C\in \mathscr{H}$$
4	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
5		2cn	$$⊢2\in ℂ$$
6	5 3	hvmulcli	$$⊢2{\cdot }_{ℎ}C\in \mathscr{H}$$
7	4 6	hvsubcli	$$⊢\left(A{+}_{ℎ}B\right){-}_{ℎ}\left(2{\cdot }_{ℎ}C\right)\in \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}$$
31	29 11	hvmulcli	$$⊢-1{\cdot }_{ℎ}\left(A{-}_{ℎ}B\right)\in \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}$$
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		4div2e2	$$⊢\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$$