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	⊢ 𝐴 ∈ ℋ
	polid2.2	⊢ 𝐵 ∈ ℋ
	polid2.3	⊢ 𝐶 ∈ ℋ
	polid2.4	⊢ 𝐷 ∈ ℋ
Assertion	polid2i	⊢ ( 𝐴 ·ih 𝐵 ) = ( ( ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )

Proof

Step	Hyp	Ref	Expression
1		polid2.1	⊢ 𝐴 ∈ ℋ
2		polid2.2	⊢ 𝐵 ∈ ℋ
3		polid2.3	⊢ 𝐶 ∈ ℋ
4		polid2.4	⊢ 𝐷 ∈ ℋ
5		4cn	⊢ 4 ∈ ℂ
6	1 2	hicli	⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
7		4ne0	⊢ 4 ≠ 0
8		2cn	⊢ 2 ∈ ℂ
9	3 4	hicli	⊢ ( 𝐶 ·ih 𝐷 ) ∈ ℂ
10	6 9	addcli	⊢ ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ∈ ℂ
11	6 9	subcli	⊢ ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ∈ ℂ
12	8 10 11	adddii	⊢ ( 2 · ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) ) = ( ( 2 · ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) + ( 2 · ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) )
13		ppncan	⊢ ( ( ( 𝐴 ·ih 𝐵 ) ∈ ℂ ∧ ( 𝐶 ·ih 𝐷 ) ∈ ℂ ∧ ( 𝐴 ·ih 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) = ( ( 𝐴 ·ih 𝐵 ) + ( 𝐴 ·ih 𝐵 ) ) )
14	6 9 6 13	mp3an	⊢ ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) = ( ( 𝐴 ·ih 𝐵 ) + ( 𝐴 ·ih 𝐵 ) )
15	6	2timesi	⊢ ( 2 · ( 𝐴 ·ih 𝐵 ) ) = ( ( 𝐴 ·ih 𝐵 ) + ( 𝐴 ·ih 𝐵 ) )
16	14 15	eqtr4i	⊢ ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) = ( 2 · ( 𝐴 ·ih 𝐵 ) )
17	16	oveq2i	⊢ ( 2 · ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) ) = ( 2 · ( 2 · ( 𝐴 ·ih 𝐵 ) ) )
18	8 8 6	mulassi	⊢ ( ( 2 · 2 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 2 · ( 2 · ( 𝐴 ·ih 𝐵 ) ) )
19		2t2e4	⊢ ( 2 · 2 ) = 4
20	19	oveq1i	⊢ ( ( 2 · 2 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 4 · ( 𝐴 ·ih 𝐵 ) )
21	17 18 20	3eqtr2ri	⊢ ( 4 · ( 𝐴 ·ih 𝐵 ) ) = ( 2 · ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) )
22	1 4	hicli	⊢ ( 𝐴 ·ih 𝐷 ) ∈ ℂ
23	3 2	hicli	⊢ ( 𝐶 ·ih 𝐵 ) ∈ ℂ
24	22 23	addcli	⊢ ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) ∈ ℂ
25	24 10 10	pnncani	⊢ ( ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) − ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) − ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) ) = ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) )
26	1 3 4 2	normlem8	⊢ ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) = ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) )
27	1 3 4 2	normlem9	⊢ ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) = ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) − ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) )
28	26 27	oveq12i	⊢ ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) = ( ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) − ( ( ( 𝐴 ·ih 𝐷 ) + ( 𝐶 ·ih 𝐵 ) ) − ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) )
29	10	2timesi	⊢ ( 2 · ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) = ( ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) )
30	25 28 29	3eqtr4i	⊢ ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) = ( 2 · ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) )
31		ax-icn	⊢ i ∈ ℂ
32	31 3	hvmulcli	⊢ ( i ·ℎ 𝐶 ) ∈ ℋ
33	31 2	hvmulcli	⊢ ( i ·ℎ 𝐵 ) ∈ ℋ
34	1 32 4 33	normlem8	⊢ ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) )
35	1 32 4 33	normlem9	⊢ ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) = ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) )
36	34 35	oveq12i	⊢ ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) = ( ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) − ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) )
37	32 33	hicli	⊢ ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ∈ ℂ
38	22 37	addcli	⊢ ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) ∈ ℂ
39	1 33	hicli	⊢ ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) ∈ ℂ
40	32 4	hicli	⊢ ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ∈ ℂ
41	39 40	addcli	⊢ ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ∈ ℂ
42	38 41 41	pnncani	⊢ ( ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) − ( ( ( 𝐴 ·ih 𝐷 ) + ( ( i ·ℎ 𝐶 ) ·ih ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) ) = ( ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) )
43	41	2timesi	⊢ ( 2 · ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) = ( ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) )
44		his5	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 ·ih 𝐵 ) ) )
45	31 1 2 44	mp3an	⊢ ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 ·ih 𝐵 ) )
46		cji	⊢ ( ∗ ‘ i ) = - i
47	46	oveq1i	⊢ ( ( ∗ ‘ i ) · ( 𝐴 ·ih 𝐵 ) ) = ( - i · ( 𝐴 ·ih 𝐵 ) )
48	45 47	eqtri	⊢ ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) = ( - i · ( 𝐴 ·ih 𝐵 ) )
49		ax-his3	⊢ ( ( i ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) = ( i · ( 𝐶 ·ih 𝐷 ) ) )
50	31 3 4 49	mp3an	⊢ ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) = ( i · ( 𝐶 ·ih 𝐷 ) )
51	48 50	oveq12i	⊢ ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) = ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) )
52	51	oveq2i	⊢ ( 2 · ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) = ( 2 · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) )
53	43 52	eqtr3i	⊢ ( ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) + ( ( 𝐴 ·ih ( i ·ℎ 𝐵 ) ) + ( ( i ·ℎ 𝐶 ) ·ih 𝐷 ) ) ) = ( 2 · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) )
54	36 42 53	3eqtri	⊢ ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) = ( 2 · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) )
55	54	oveq2i	⊢ ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) = ( i · ( 2 · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) )
56		negicn	⊢ - i ∈ ℂ
57	56 6	mulcli	⊢ ( - i · ( 𝐴 ·ih 𝐵 ) ) ∈ ℂ
58	31 9	mulcli	⊢ ( i · ( 𝐶 ·ih 𝐷 ) ) ∈ ℂ
59	57 58	addcli	⊢ ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ∈ ℂ
60	8 31 59	mul12i	⊢ ( 2 · ( i · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) ) = ( i · ( 2 · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) )
61	31 57 58	adddii	⊢ ( i · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) = ( ( i · ( - i · ( 𝐴 ·ih 𝐵 ) ) ) + ( i · ( i · ( 𝐶 ·ih 𝐷 ) ) ) )
62	31 31	mulneg2i	⊢ ( i · - i ) = - ( i · i )
63		ixi	⊢ ( i · i ) = - 1
64	63	negeqi	⊢ - ( i · i ) = - - 1
65		negneg1e1	⊢ - - 1 = 1
66	62 64 65	3eqtri	⊢ ( i · - i ) = 1
67	66	oveq1i	⊢ ( ( i · - i ) · ( 𝐴 ·ih 𝐵 ) ) = ( 1 · ( 𝐴 ·ih 𝐵 ) )
68	31 56 6	mulassi	⊢ ( ( i · - i ) · ( 𝐴 ·ih 𝐵 ) ) = ( i · ( - i · ( 𝐴 ·ih 𝐵 ) ) )
69	6	mulid2i	⊢ ( 1 · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐴 ·ih 𝐵 )
70	67 68 69	3eqtr3i	⊢ ( i · ( - i · ( 𝐴 ·ih 𝐵 ) ) ) = ( 𝐴 ·ih 𝐵 )
71	63	oveq1i	⊢ ( ( i · i ) · ( 𝐶 ·ih 𝐷 ) ) = ( - 1 · ( 𝐶 ·ih 𝐷 ) )
72	31 31 9	mulassi	⊢ ( ( i · i ) · ( 𝐶 ·ih 𝐷 ) ) = ( i · ( i · ( 𝐶 ·ih 𝐷 ) ) )
73	9	mulm1i	⊢ ( - 1 · ( 𝐶 ·ih 𝐷 ) ) = - ( 𝐶 ·ih 𝐷 )
74	71 72 73	3eqtr3i	⊢ ( i · ( i · ( 𝐶 ·ih 𝐷 ) ) ) = - ( 𝐶 ·ih 𝐷 )
75	70 74	oveq12i	⊢ ( ( i · ( - i · ( 𝐴 ·ih 𝐵 ) ) ) + ( i · ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) = ( ( 𝐴 ·ih 𝐵 ) + - ( 𝐶 ·ih 𝐷 ) )
76	6 9	negsubi	⊢ ( ( 𝐴 ·ih 𝐵 ) + - ( 𝐶 ·ih 𝐷 ) ) = ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) )
77	61 75 76	3eqtri	⊢ ( i · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) = ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) )
78	77	oveq2i	⊢ ( 2 · ( i · ( ( - i · ( 𝐴 ·ih 𝐵 ) ) + ( i · ( 𝐶 ·ih 𝐷 ) ) ) ) ) = ( 2 · ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) )
79	55 60 78	3eqtr2i	⊢ ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) = ( 2 · ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) )
80	30 79	oveq12i	⊢ ( ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) = ( ( 2 · ( ( 𝐴 ·ih 𝐵 ) + ( 𝐶 ·ih 𝐷 ) ) ) + ( 2 · ( ( 𝐴 ·ih 𝐵 ) − ( 𝐶 ·ih 𝐷 ) ) ) )
81	12 21 80	3eqtr4i	⊢ ( 4 · ( 𝐴 ·ih 𝐵 ) ) = ( ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) )
82	5 6 7 81	mvllmuli	⊢ ( 𝐴 ·ih 𝐵 ) = ( ( ( ( ( 𝐴 +ℎ 𝐶 ) ·ih ( 𝐷 +ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐶 ) ·ih ( 𝐷 −ℎ 𝐵 ) ) ) + ( i · ( ( ( 𝐴 +ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 +ℎ ( i ·ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ ( i ·ℎ 𝐶 ) ) ·ih ( 𝐷 −ℎ ( i ·ℎ 𝐵 ) ) ) ) ) ) / 4 )