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		4d2e2	⊢ ( 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 ) )