This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidi ⊢ ( 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 )