Theorem polid2 8945

Description: Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63.

Hypotheses

Ref	Expression
polid2.1	|- A e. H~
polid2.2	|- B e. H~
polid2.3	|- C e. H~
polid2.4	|- D e. H~

Assertion

Ref	Expression
polid2	|- (A .ih B) = (((((A +h C) .ih (D +h B)) - ((A -h C) .ih (D -h B))) + (i x. (((A +h (i .h C)) .ih (D +h (i .h B))) - ((A -h (i .h C)) .ih (D -h (i .h B)))))) / 4)

Proof of Theorem polid2

Step	Hyp	Ref	Expression
1		4re 5929	. . . 4 |- 4 e. RR
2	1	recn 5286	. . 3 |- 4 e. CC
3		polid2.1	. . . 4 |- A e. H~
4		polid2.2	. . . 4 |- B e. H~
5	3, 4	hicl 8869	. . 3 |- (A .ih B) e. CC
6		4pos 5939	. . . 4 |- 0 < 4
7	1, 6	gt0ne0i 5591	. . 3 |- 4 =/= 0
8	2, 5, 7	divcan3 5714	. 2 |- ((4 x. (A .ih B)) / 4) = (A .ih B)
9		2cn 5927	. . . . 5 |- 2 e. CC
10		polid2.3	. . . . . . 7 |- C e. H~
11		polid2.4	. . . . . . 7 |- D e. H~
12	10, 11	hicl 8869	. . . . . 6 |- (C .ih D) e. CC
13	5, 12	addcl 5292	. . . . 5 |- ((A .ih B) + (C .ih D)) e. CC
14	5, 12	subcl 5338	. . . . 5 |- ((A .ih B) - (C .ih D)) e. CC
15	9, 13, 14	adddi 5298	. . . 4 |- (2 x. (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D)))) = ((2 x. ((A .ih B) + (C .ih D))) + (2 x. ((A .ih B) - (C .ih D))))
16		ppncant 5453	. . . . . . . 8 |- (((A .ih B) e. CC /\ (C .ih D) e. CC /\ (A .ih B) e. CC) -> (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D))) = ((A .ih B) + (A .ih B)))
17	5, 12, 5, 16	mp3an 913	. . . . . . 7 |- (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D))) = ((A .ih B) + (A .ih B))
18	5	2times 5950	. . . . . . 7 |- (2 x. (A .ih B)) = ((A .ih B) + (A .ih B))
19	17, 18	eqtr4 1490	. . . . . 6 |- (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D))) = (2 x. (A .ih B))
20	19	opreq2i 3957	. . . . 5 |- (2 x. (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D)))) = (2 x. (2 x. (A .ih B)))
21	9, 9, 5	mulass 5297	. . . . 5 |- ((2 x. 2) x. (A .ih B)) = (2 x. (2 x. (A .ih B)))
22		2t2e4 5969	. . . . . 6 |- (2 x. 2) = 4
23	22	opreq1i 3956	. . . . 5 |- ((2 x. 2) x. (A .ih B)) = (4 x. (A .ih B))
24	20, 21, 23	3eqtr2r 1494	. . . 4 |- (4 x. (A .ih B)) = (2 x. (((A .ih B) + (C .ih D)) + ((A .ih B) - (C .ih D))))
25	3, 11	hicl 8869	. . . . . . . 8 |- (A .ih D) e. CC
26	10, 4	hicl 8869	. . . . . . . 8 |- (C .ih B) e. CC
27	25, 26	addcl 5292	. . . . . . 7 |- ((A .ih D) + (C .ih B)) e. CC
28	27, 13, 13	pnncan 5454	. . . . . 6 |- ((((A .ih D) + (C .ih B)) + ((A .ih B) + (C .ih D))) - (((A .ih D) + (C .ih B)) - ((A .ih B) + (C .ih D)))) = (((A .ih B) + (C .ih D)) + ((A .ih B) + (C .ih D)))
29	3, 10, 11, 4	normlem8 8904	. . . . . . 7 |- ((A +h C) .ih (D +h B)) = (((A .ih D) + (C .ih B)) + ((A .ih B) + (C .ih D)))
30	3, 10, 11, 4	normlem9 8905	. . . . . . 7 |- ((A -h C) .ih (D -h B)) = (((A .ih D) + (C .ih B)) - ((A .ih B) + (C .ih D)))
31	29, 30	opreq12i 3958	. . . . . 6 |- (((A +h C) .ih (D +h B)) - ((A -h C) .ih (D -h B))) = ((((A .ih D) + (C .ih B)) + ((A .ih B) + (C .ih D))) - (((A .ih D) + (C .ih B)) - ((A .ih B) + (C .ih D))))
32	13	2times 5950	. . . . . 6 |- (2 x. ((A .ih B) + (C .ih D))) = (((A .ih B) + (C .ih D)) + ((A .ih B) + (C .ih D)))
33	28, 31, 32	3eqtr4 1497	. . . . 5 |- (((A +h C) .ih (D +h B)) - ((A -h C) .ih (D -h B))) = (2 x. ((A .ih B) + (C .ih D)))
34		axicn 5242	. . . . . . . . . . 11 |- i e. CC
35	34, 10	hvmulcl 8805	. . . . . . . . . 10 |- (i .h C) e. H~
36	34, 4	hvmulcl 8805	. . . . . . . . . 10 |- (i .h B) e. H~
37	3, 35, 11, 36	normlem8 8904	. . . . . . . . 9 |- ((A +h (i .h C)) .ih (D +h (i .h B))) = (((A .ih D) + ((i .h C) .ih (i .h B))) + ((A .ih (i .h B)) + ((i .h C) .ih D)))
38	3, 35, 11, 36	normlem9 8905	. . . . . . . . 9 |- ((A -h (i .h C)) .ih (D -h (i .h B))) = (((A .ih D) + ((i .h C) .ih (i .h B))) - ((A .ih (i .h B)) + ((i .h C) .ih D)))
39	37, 38	opreq12i 3958	. . . . . . . 8 |- (((A +h (i .h C)) .ih (D +h (i .h B))) - ((A -h (i .h C)) .ih (D -h (i .h B)))) = ((((A .ih D) + ((i .h C) .ih (i .h B))) + ((A .ih (i .h B)) + ((i .h C) .ih D))) - (((A .ih D) + ((i .h C) .ih (i .h B))) - ((A .ih (i .h B)) + ((i .h C) .ih D))))
40	35, 36	hicl 8869	. . . . . . . . . 10 |- ((i .h C) .ih (i .h B)) e. CC
41	25, 40	addcl 5292	. . . . . . . . 9 |- ((A .ih D) + ((i .h C) .ih (i .h B))) e. CC
42	3, 36	hicl 8869	. . . . . . . . . 10 |- (A .ih (i .h B)) e. CC
43	35, 11	hicl 8869	. . . . . . . . . 10 |- ((i .h C) .ih D) e. CC
44	42, 43	addcl 5292	. . . . . . . . 9 |- ((A .ih (i .h B)) + ((i .h C) .ih D)) e. CC
45	41, 44, 44	pnncan 5454	. . . . . . . 8 |- ((((A .ih D) + ((i .h C) .ih (i .h B))) + ((A .ih (i .h B)) + ((i .h C) .ih D))) - (((A .ih D) + ((i .h C) .ih (i .h B))) - ((A .ih (i .h B)) + ((i .h C) .ih D)))) = (((A .ih (i .h B)) + ((i .h C) .ih D)) + ((A .ih (i .h B)) + ((i .h C) .ih D)))
46	44	2times 5950	. . . . . . . . 9 |- (2 x. ((A .ih (i .h B)) + ((i .h C) .ih D))) = (((A .ih (i .h B)) + ((i .h C) .ih D)) + ((A .ih (i .h B)) + ((i .h C) .ih D)))
47		his5t 8874	. . . . . . . . . . . . 13 |- ((i e. CC /\ A e. H~ /\ B e. H~) -> (A .ih (i .h B)) = ((*` i) x. (A .ih B)))
48	34, 3, 4, 47	mp3an 913	. . . . . . . . . . . 12 |- (A .ih (i .h B)) = ((*` i) x. (A .ih B))
49		cji 6762	. . . . . . . . . . . . 13 |- (*` i) = -ui
50	49	opreq1i 3956	. . . . . . . . . . . 12 |- ((*` i) x. (A .ih B)) = (-ui x. (A .ih B))
51	48, 50	eqtr 1487	. . . . . . . . . . 11 |- (A .ih (i .h B)) = (-ui x. (A .ih B))
52		ax-his3 8872	. . . . . . . . . . . 12 |- ((i e. CC /\ C e. H~ /\ D e. H~) -> ((i .h C) .ih D) = (i x. (C .ih D)))
53	34, 10, 11, 52	mp3an 913	. . . . . . . . . . 11 |- ((i .h C) .ih D) = (i x. (C .ih D))
54	51, 53	opreq12i 3958	. . . . . . . . . 10 |- ((A .ih (i .h B)) + ((i .h C) .ih D)) = ((-ui x. (A .ih B)) + (i x. (C .ih D)))
55	54	opreq2i 3957	. . . . . . . . 9 |- (2 x. ((A .ih (i .h B)) + ((i .h C) .ih D))) = (2 x. ((-ui x. (A .ih B)) + (i x. (C .ih D))))
56	46, 55	eqtr3 1489	. . . . . . . 8 |- (((A .ih (i .h B)) + ((i .h C) .ih D)) + ((A .ih (i .h B)) + ((i .h C) .ih D))) = (2 x. ((-ui x. (A .ih B)) + (i x. (C .ih D))))
57	39, 45, 56	3eqtr 1491	. . . . . . 7 |- (((A +h (i .h C)) .ih (D +h (i .h B))) - ((A -h (i .h C)) .ih (D -h (i .h B)))) = (2 x. ((-ui x. (A .ih B)) + (i x. (C .ih D))))
58	57	opreq2i 3957	. . . . . 6 |- (i x. (((A +h (i .h C)) .ih (D +h (i .h