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