Theorem polid2i

Description: Generalized polarization identity. Generalization of Exercise 4(a) of ReedSimon p. 63. (Contributed by NM, 30-Jun-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polid2.1	|- A e. ~H
	polid2.2	|- B e. ~H
	polid2.3	|- C e. ~H
	polid2.4	|- D e. ~H
Assertion	polid2i	|- ( 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

Step	Hyp	Ref	Expression
1		polid2.1	|- A e. ~H
2		polid2.2	|- B e. ~H
3		polid2.3	|- C e. ~H
4		polid2.4	|- D e. ~H
5		4cn	|- 4 e. CC
6	1 2	hicli	|- ( A .ih B ) e. CC
7		4ne0	|- 4 =/= 0
8		2cn	|- 2 e. CC
9	3 4	hicli	|- ( C .ih D ) e. CC
10	6 9	addcli	|- ( ( A .ih B ) + ( C .ih D ) ) e. CC
11	6 9	subcli	|- ( ( A .ih B ) - ( C .ih D ) ) e. CC
12	8 10 11	adddii	|- ( 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 ) ) ) )
13		ppncan	|- ( ( ( 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 ) ) )
14	6 9 6 13	mp3an	|- ( ( ( A .ih B ) + ( C .ih D ) ) + ( ( A .ih B ) - ( C .ih D ) ) ) = ( ( A .ih B ) + ( A .ih B ) )
15	6	2timesi	|- ( 2 x. ( A .ih B ) ) = ( ( A .ih B ) + ( A .ih B ) )
16	14 15	eqtr4i	|- ( ( ( A .ih B ) + ( C .ih D ) ) + ( ( A .ih B ) - ( C .ih D ) ) ) = ( 2 x. ( A .ih B ) )
17	16	oveq2i	|- ( 2 x. ( ( ( A .ih B ) + ( C .ih D ) ) + ( ( A .ih B ) - ( C .ih D ) ) ) ) = ( 2 x. ( 2 x. ( A .ih B ) ) )
18	8 8 6	mulassi	|- ( ( 2 x. 2 ) x. ( A .ih B ) ) = ( 2 x. ( 2 x. ( A .ih B ) ) )
19		2t2e4	|- ( 2 x. 2 ) = 4
20	19	oveq1i	|- ( ( 2 x. 2 ) x. ( A .ih B ) ) = ( 4 x. ( A .ih B ) )
21	17 18 20	3eqtr2ri	|- ( 4 x. ( A .ih B ) ) = ( 2 x. ( ( ( A .ih B ) + ( C .ih D ) ) + ( ( A .ih B ) - ( C .ih D ) ) ) )
22	1 4	hicli	|- ( A .ih D ) e. CC
23	3 2	hicli	|- ( C .ih B ) e. CC
24	22 23	addcli	|- ( ( A .ih D ) + ( C .ih B ) ) e. CC
25	24 10 10	pnncani	|- ( ( ( ( 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 ) ) )
26	1 3 4 2	normlem8	|- ( ( A +h C ) .ih ( D +h B ) ) = ( ( ( A .ih D ) + ( C .ih B ) ) + ( ( A .ih B ) + ( C .ih D ) ) )
27	1 3 4 2	normlem9	|- ( ( A -h C ) .ih ( D -h B ) ) = ( ( ( A .ih D ) + ( C .ih B ) ) - ( ( A .ih B ) + ( C .ih D ) ) )
28	26 27	oveq12i	|- ( ( ( 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 ) ) ) )
29	10	2timesi	|- ( 2 x. ( ( A .ih B ) + ( C .ih D ) ) ) = ( ( ( A .ih B ) + ( C .ih D ) ) + ( ( A .ih B ) + ( C .ih D ) ) )
30	25 28 29	3eqtr4i	|- ( ( ( A +h C ) .ih ( D +h B ) ) - ( ( A -h C ) .ih ( D -h B ) ) ) = ( 2 x. ( ( A .ih B ) + ( C .ih D ) ) )
31		ax-icn	|- _i e. CC
32	31 3	hvmulcli	|- ( _i .h C ) e. ~H
33	31 2	hvmulcli	|- ( _i .h B ) e. ~H
34	1 32 4 33	normlem8	|- ( ( 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 ) ) )
35	1 32 4 33	normlem9	|- ( ( 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 ) ) )
36	34 35	oveq12i	|- ( ( ( 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 ) ) ) )
37	32 33	hicli	|- ( ( _i .h C ) .ih ( _i .h B ) ) e. CC
38	22 37	addcli	|- ( ( A .ih D ) + ( ( _i .h C ) .ih ( _i .h B ) ) ) e. CC
39	1 33	hicli	|- ( A .ih ( _i .h B ) ) e. CC
40	32 4	hicli	|- ( ( _i .h C ) .ih D ) e. CC
41	39 40	addcli	|- ( ( A .ih ( _i .h B ) ) + ( ( _i .h C ) .ih D ) ) e. CC
42	38 41 41	pnncani	|- ( ( ( ( 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 ) ) )
43	41	2timesi	|- ( 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 ) ) )
44		his5	|- ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( _i .h B ) ) = ( ( * ` _i ) x. ( A .ih B ) ) )
45	31 1 2 44	mp3an	|- ( A .ih ( _i .h B ) ) = ( ( * ` _i ) x. ( A .ih B ) )
46		cji	|- ( * ` _i ) = -u _i
47	46	oveq1i	|- ( ( * ` _i ) x. ( A .ih B ) ) = ( -u _i x. ( A .ih B ) )
48	45 47	eqtri	|- ( A .ih ( _i .h B ) ) = ( -u _i x. ( A .ih B ) )
49		ax-his3	|- ( ( _i e. CC /\ C e. ~H /\ D e. ~H ) -> ( ( _i .h C ) .ih D ) = ( _i x. ( C .ih D ) ) )
50	31 3 4 49	mp3an	|- ( ( _i .h C ) .ih D ) = ( _i x. ( C .ih D ) )
51	48 50	oveq12i	|- ( ( A .ih ( _i .h B ) ) + ( ( _i .h C ) .ih D ) ) = ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) )
52	51	oveq2i	|- ( 2 x. ( ( A .ih ( _i .h B ) ) + ( ( _i .h C ) .ih D ) ) ) = ( 2 x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) )
53	43 52	eqtr3i	|- ( ( ( A .ih ( _i .h B ) ) + ( ( _i .h C ) .ih D ) ) + ( ( A .ih ( _i .h B ) ) + ( ( _i .h C ) .ih D ) ) ) = ( 2 x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) )
54	36 42 53	3eqtri	|- ( ( ( A +h ( _i .h C ) ) .ih ( D +h ( _i .h B ) ) ) - ( ( A -h ( _i .h C ) ) .ih ( D -h ( _i .h B ) ) ) ) = ( 2 x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) )
55	54	oveq2i	|- ( _i x. ( ( ( A +h ( _i .h C ) ) .ih ( D +h ( _i .h B ) ) ) - ( ( A -h ( _i .h C ) ) .ih ( D -h ( _i .h B ) ) ) ) ) = ( _i x. ( 2 x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) )
56		negicn	|- -u _i e. CC
57	56 6	mulcli	|- ( -u _i x. ( A .ih B ) ) e. CC
58	31 9	mulcli	|- ( _i x. ( C .ih D ) ) e. CC
59	57 58	addcli	|- ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) e. CC
60	8 31 59	mul12i	|- ( 2 x. ( _i x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) ) = ( _i x. ( 2 x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) )
61	31 57 58	adddii	|- ( _i x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) = ( ( _i x. ( -u _i x. ( A .ih B ) ) ) + ( _i x. ( _i x. ( C .ih D ) ) ) )
62	31 31	mulneg2i	|- ( _i x. -u _i ) = -u ( _i x. _i )
63		ixi	|- ( _i x. _i ) = -u 1
64	63	negeqi	|- -u ( _i x. _i ) = -u -u 1
65		negneg1e1	|- -u -u 1 = 1
66	62 64 65	3eqtri	|- ( _i x. -u _i ) = 1
67	66	oveq1i	|- ( ( _i x. -u _i ) x. ( A .ih B ) ) = ( 1 x. ( A .ih B ) )
68	31 56 6	mulassi	|- ( ( _i x. -u _i ) x. ( A .ih B ) ) = ( _i x. ( -u _i x. ( A .ih B ) ) )
69	6	mulid2i	|- ( 1 x. ( A .ih B ) ) = ( A .ih B )
70	67 68 69	3eqtr3i	|- ( _i x. ( -u _i x. ( A .ih B ) ) ) = ( A .ih B )
71	63	oveq1i	|- ( ( _i x. _i ) x. ( C .ih D ) ) = ( -u 1 x. ( C .ih D ) )
72	31 31 9	mulassi	|- ( ( _i x. _i ) x. ( C .ih D ) ) = ( _i x. ( _i x. ( C .ih D ) ) )
73	9	mulm1i	|- ( -u 1 x. ( C .ih D ) ) = -u ( C .ih D )
74	71 72 73	3eqtr3i	|- ( _i x. ( _i x. ( C .ih D ) ) ) = -u ( C .ih D )
75	70 74	oveq12i	|- ( ( _i x. ( -u _i x. ( A .ih B ) ) ) + ( _i x. ( _i x. ( C .ih D ) ) ) ) = ( ( A .ih B ) + -u ( C .ih D ) )
76	6 9	negsubi	|- ( ( A .ih B ) + -u ( C .ih D ) ) = ( ( A .ih B ) - ( C .ih D ) )
77	61 75 76	3eqtri	|- ( _i x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) = ( ( A .ih B ) - ( C .ih D ) )
78	77	oveq2i	|- ( 2 x. ( _i x. ( ( -u _i x. ( A .ih B ) ) + ( _i x. ( C .ih D ) ) ) ) ) = ( 2 x. ( ( A .ih B ) - ( C .ih D ) ) )
79	55 60 78	3eqtr2i	|- ( _i x. ( ( ( A +h ( _i .h C ) ) .ih ( D +h ( _i .h B ) ) ) - ( ( A -h ( _i .h C ) ) .ih ( D -h ( _i .h B ) ) ) ) ) = ( 2 x. ( ( A .ih B ) - ( C .ih D ) ) )
80	30 79	oveq12i	|- ( ( ( ( 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 ) ) ) ) ) ) = ( ( 2 x. ( ( A .ih B ) + ( C .ih D ) ) ) + ( 2 x. ( ( A .ih B ) - ( C .ih D ) ) ) )
81	12 21 80	3eqtr4i	|- ( 4 x. ( 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 ) ) ) ) ) )
82	5 6 7 81	mvllmuli	|- ( 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 )