Theorem normpar2 5100

Description: Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100.

Hypotheses

Ref	Expression
normpar2.1	|- A e. H~
normpar2.2	|- B e. H~
normpar2.3	|- C e. H~

Assertion

Ref	Expression
normpar2	|- ((norm` (A -v B))^2) = (((2 x. ((norm` (A -v C))^2)) + (2 x. ((norm` (B -v C))^2))) - ((norm` ((A +v B) -v (2 .s C)))^2))

Proof of Theorem normpar2

Step	Hyp	Ref	Expression
1		4re 4473	. . . . . . 7 |- 4 e. RR
2	1	recn 4098	. . . . . 6 |- 4 e. CC
3		normpar2.1	. . . . . . . . . 10 |- A e. H~
4		normpar2.3	. . . . . . . . . 10 |- C e. H~
5	3, 4	hvsubcl 5002	. . . . . . . . 9 |- (A -v C) e. H~
6	5	normcl 5081	. . . . . . . 8 |- (norm` (A -v C)) e. RR
7	6	sqrecl 4699	. . . . . . 7 |- ((norm` (A -v C))^2) e. RR
8	7	recn 4098	. . . . . 6 |- ((norm` (A -v C))^2) e. CC
9	2, 8	mulcl 4105	. . . . 5 |- (4 x. ((norm` (A -v C))^2)) e. CC
10		normpar2.2	. . . . . . . . . 10 |- B e. H~
11	10, 4	hvsubcl 5002	. . . . . . . . 9 |- (B -v C) e. H~
12	11	normcl 5081	. . . . . . . 8 |- (norm` (B -v C)) e. RR
13	12	sqrecl 4699	. . . . . . 7 |- ((norm` (B -v C))^2) e. RR
14	13	recn 4098	. . . . . 6 |- ((norm` (B -v C))^2) e. CC
15	2, 14	mulcl 4105	. . . . 5 |- (4 x. ((norm` (B -v C))^2)) e. CC
16		2cn 4471	. . . . 5 |- 2 e. CC
17		2re 4470	. . . . . 6 |- 2 e. RR
18		2pos 4479	. . . . . 6 |- 0 < 2
19	17, 18	gt0ne0i 4345	. . . . 5 |- 2 =/= 0
20	9, 15, 16, 19	divdistr 4243	. . . 4 |- (((4 x. ((norm` (A -v C))^2)) + (4 x. ((norm` (B -v C))^2))) / 2) = (((4 x. ((norm` (A -v C))^2)) / 2) + ((4 x. ((norm` (B -v C))^2)) / 2))
21	9, 15	addcom 4106	. . . . . . . 8 |- ((4 x. ((norm` (A -v C))^2)) + (4 x. ((norm` (B -v C))^2))) = ((4 x. ((norm` (B -v C))^2)) + (4 x. ((norm` (A -v C))^2)))
22	3, 10	hvaddcl 4999	. . . . . . . . . . . . . . . . 17 |- (A +v B) e. H~
23	16, 4	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 |- (2 .s C) e. H~
24	22, 23	hvsubcl 5002	. . . . . . . . . . . . . . . 16 |- ((A +v B) -v (2 .s C)) e. H~
25	3, 10	hvsubcl 5002	. . . . . . . . . . . . . . . 16 |- (A -v B) e. H~
26	24, 25	hvsubval 5001	. . . . . . . . . . . . . . 15 |- (((A +v B) -v (2 .s C)) -v (A -v B)) = (((A +v B) -v (2 .s C)) +v (-u1 .s (A -v B)))
27	22, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 |- ((A +v B) -v (2 .s C)) = ((A +v B) +v (-u1 .s (2 .s C)))
28	27	opreq1i 3009	. . . . . . . . . . . . . . 15 |- (((A +v B) -v (2 .s C)) +v (-u1 .s (A -v B))) = (((A +v B) +v (-u1 .s (2 .s C))) +v (-u1 .s (A -v B)))
29	3, 10	hvcom 5000	. . . . . . . . . . . . . . . . . . 19 |- (A +v B) = (B +v A)
30	3, 10	hvnegdi 5034	. . . . . . . . . . . . . . . . . . 19 |- (-u1 .s (A -v B)) = (B -v A)
31	29, 30	opreq12i 3011	. . . . . . . . . . . . . . . . . 18 |- ((A +v B) +v (-u1 .s (A -v B))) = ((B +v A) +v (B -v A))
32	10, 3	hvsubcan2 5036	. . . . . . . . . . . . . . . . . 18 |- ((B +v A) +v (B -v A)) = (2 .s B)
33	31, 32	eqtr 1119	. . . . . . . . . . . . . . . . 17 |- ((A +v B) +v (-u1 .s (A -v B))) = (2 .s B)
34	33	opreq1i 3009	. . . . . . . . . . . . . . . 16 |- (((A +v B) +v (-u1 .s (A -v B))) +v (-u1 .s (2 .s C))) = ((2 .s B) +v (-u1 .s (2 .s C)))
35		1cn 4101	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
36	35	negcl 4142	. . . . . . . . . . . . . . . . . 18 |- -u1 e. CC
37	36, 23	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 |- (-u1 .s (2 .s C)) e. H~
38	36, 25	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 |- (-u1 .s (A -v B)) e. H~
39	22, 37, 38	hvadd23 5026	. . . . . . . . . . . . . . . 16 |- (((A +v B) +v (-u1 .s (2 .s C))) +v (-u1 .s (A -v B))) = (((A +v B) +v (-u1 .s (A -v B))) +v (-u1 .s (2 .s C)))
40	16, 10	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 |- (2 .s B) e. H~
41	40, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 |- ((2 .s B) -v (2 .s C)) = ((2 .s B) +v (-u1 .s (2 .s C)))
42	34, 39, 41	3eqtr4 1126	. . . . . . . . . . . . . . 15 |- (((A +v B) +v (-u1 .s (2 .s C))) +v (-u1 .s (A -v B))) = ((2 .s B) -v (2 .s C))
43	26, 28, 42	3eqtr 1123	. . . . . . . . . . . . . 14 |- (((A +v B) -v (2 .s C)) -v (A -v B)) = ((2 .s B) -v (2 .s C))
44	16, 10, 4	hvsubdistr1 5024	. . . . . . . . . . . . . 14 |- (2 .s (B -v C)) = ((2 .s B) -v (2 .s C))
45	43, 44	eqtr4 1122	. . . . . . . . . . . . 13 |- (((A +v B) -v (2 .s C)) -v (A -v B)) = (2 .s (B -v C))
46	45	fveq2i 2835	. . . . . . . . . . . 12 |- (norm` (((A +v B) -v (2 .s C)) -v (A -v B))) = (norm` (2 .s (B -v C)))
47	16, 11	norm-iii 5087	. . . . . . . . . . . 12 |- (norm` (2 .s (B -v C))) = ((abs` 2) x. (norm` (B -v C)))
48		ax0re 4063	. . . . . . . . . . . . . . 15 |- 0 e. RR
49	48, 17, 18	ltlei 4303	. . . . . . . . . . . . . 14 |- 0 <_ 2
50	17	absid 4850	. . . . . . . . . . . . . 14 |- (0 <_ 2 -> (abs` 2) = 2)
51	49, 50	ax-mp 6	. . . . . . . . . . . . 13 |- (abs` 2) = 2
52	51	opreq1i 3009	. . . . . . . . . . . 12 |- ((abs` 2) x. (norm` (B -v C))) = (2 x. (norm` (B -v C)))
53	46, 47, 52	3eqtr 1123	. . . . . . . . . . 11 |- (norm` (((A +v B) -v (2 .s C)) -v (A -v B))) = (2 x. (norm` (B -v C)))
54	53	opreq1i 3009	. . . . . . . . . 10 |- ((norm` (((A +v B) -v (2 .s C)) -v (A -v B)))^2) = ((2 x. (norm` (B -v C)))^2)
55	12	recn 4098	. . . . . . . . . . 11 |- (norm` (B -v C)) e. CC
56	16, 55	sqmul 4688	. . . . . . . . . 10 |- ((2 x. (norm` (B -v C)))^2) = ((2^2) x. ((norm` (B -v C))^2))
57		sq2 4710	. . . . . . . . . . 11 |- (2^2) = 4
58	57	opreq1i 3009	. . . . . . . . . 10 |- ((2^2) x. ((norm` (B -v C))^2)) = (4 x. ((norm` (B -v C))^2))
59	54, 56, 58	3eqtr 1123	. . . . . . . . 9 |- ((norm` (((A +v B) -v (2 .s C)) -v (A -v B)))^2) = (4 x. ((norm` (B -v C))^2))
60	27	opreq1i 3009	. . . . . . . . . . . . . . 15 |- (((A +v B) -v (2 .s C)) +v (A -v B)) = (((A +v B) +v (-u1 .s (2 .s C))) +v (A -v B))
61	22, 37, 25	hvadd23 5026	. . . . . . . . . . . . . . 15 |- (((A +v B) +v (-u1 .s (2 .s C))) +v (A -v B)) = (((A +v B) +v (A -v B)) +v (-u1 .s (2 .s C)))
62	3, 10	hvsubcan2 5036	. . . . . . . . . . . . . . . . 17 |- ((A +v B) +v (A -v B)) = (2 .s A)
63	62	opreq1i 3009	. . . . . . . . . . . . . . . 16 |- (((A +v B) +v (A -v B)) +v (-u1 .s (2 .s C))) = ((2 .s A) +v (-u1 .s (2 .s C)))
64	16, 3	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 |- (2 .s A) e. H~
65	64, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 |- ((2 .s A) -v (2 .s C)) = ((2 .s A) +v (-u1 .s (2 .s C)))
66	63, 65	eqtr4 1122	. . . . . . . . . . . . . . 15 |- (((A +v B) +v (A -v B)) +v (-u1 .s (2 .s C))) = ((2 .s A) -v (2 .s C))
67	60, 61, 66	3eqtr 1123	. . . . . . . . . . . . . 14 |- (((A +v B) -v (2 .s C)) +v (A -v B)) = ((2 .s A) -v (2 .s C))
68	16, 3, 4	hvsubdistr1 5024	. . . . . . . . . . . . . 14 |- (2 .s (A -v C)) = ((2 .s A) -v (2 .s C))
69	67, 68	eqtr4 1122	. . . . . . . . . . . . 13 |- (((A +v B) -v (2 .s C)) +v (A -v B)) = (2 .s (A -v C))
70	69	fveq2i 2835	. . . . . . . . . . . 12 |- (norm` (((A +v B) -v (2 .s C)) +v (A -v B))) = (norm` (2 .s (A -v C)))
71	16, 5	norm-iii 5087	. . . . . . . . . . . 12 |- (norm` (2 .s (A -v C))) = ((abs` 2) x. (norm` (A -v C)))
72	51	opreq1i 3009	. . . . . . . . . . . 12 |- ((abs` 2) x. (norm` (A -v C))) = (2 x. (norm` (A -v C)))
73	70, 71, 72	3eqtr 1123	. . . . . . . . . . 11 |- (norm` (((A +v B) -v (2 .s C)) +v (A -v B))) = (2 x. (norm` (A -v C)))
74	73	opreq1i 3009	. . . . . . . . . 10 |- ((norm` (((A +v B) -v (2 .s C)) +v (A -v B)))^2) = ((2 x. (norm` (A -v C)))^2)
75	6	recn 4098	. . . . . . . . . . 11 |- (norm` (A -v C)) e. CC
76	16, 75	sqmul 4688	. . . . . . . . . 10 |- ((2 x. (norm` (A -v C)))^2) = ((2^2) x. ((norm` (A -v C))^2))
77	57	opreq1i 3009	. . . . . . . . . 10 |- ((2^2) x. ((norm` (A