Metamath Proof Explorer

Theorem lnophmlem2

Description: Lemma for lnophmi . (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnophmlem.1 
|- A e. ~H
lnophmlem.2 
|- B e. ~H
lnophmlem.3 
|- T e. LinOp
lnophmlem.4 
|- A. x e. ~H ( x .ih ( T ` x ) ) e. RR
Assertion lnophmlem2 
|- ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B )

Proof

Step Hyp Ref Expression
1 lnophmlem.1 
 |-  A e. ~H
2 lnophmlem.2 
 |-  B e. ~H
3 lnophmlem.3 
 |-  T e. LinOp
4 lnophmlem.4 
 |-  A. x e. ~H ( x .ih ( T ` x ) ) e. RR
5 3 lnopfi 
 |-  T : ~H --> ~H
6 5 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. ~H )
7 1 6 ax-mp 
 |-  ( T ` A ) e. ~H
8 5 ffvelcdmi 
 |-  ( B e. ~H -> ( T ` B ) e. ~H )
9 2 8 ax-mp 
 |-  ( T ` B ) e. ~H
10 2 7 1 9 polid2i 
 |-  ( B .ih ( T ` A ) ) = ( ( ( ( ( B +h A ) .ih ( ( T ` B ) +h ( T ` A ) ) ) - ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) ) + ( _i x. ( ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) - ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) ) ) ) / 4 )
11 2 1 hvcomi 
 |-  ( B +h A ) = ( A +h B )
12 9 7 hvcomi 
 |-  ( ( T ` B ) +h ( T ` A ) ) = ( ( T ` A ) +h ( T ` B ) )
13 3 lnopaddi 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )
14 1 2 13 mp2an 
 |-  ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) )
15 12 14 eqtr4i 
 |-  ( ( T ` B ) +h ( T ` A ) ) = ( T ` ( A +h B ) )
16 11 15 oveq12i 
 |-  ( ( B +h A ) .ih ( ( T ` B ) +h ( T ` A ) ) ) = ( ( A +h B ) .ih ( T ` ( A +h B ) ) )
17 2 1 9 7 hisubcomi 
 |-  ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) = ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) )
18 3 lnopsubi 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) ) )
19 1 2 18 mp2an 
 |-  ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) )
20 19 oveq2i 
 |-  ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) = ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) )
21 17 20 eqtr4i 
 |-  ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) = ( ( A -h B ) .ih ( T ` ( A -h B ) ) )
22 16 21 oveq12i 
 |-  ( ( ( B +h A ) .ih ( ( T ` B ) +h ( T ` A ) ) ) - ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) ) = ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) )
23 ax-icn 
 |-  _i e. CC
24 23 2 hvmulcli 
 |-  ( _i .h B ) e. ~H
25 1 24 hvsubcli 
 |-  ( A -h ( _i .h B ) ) e. ~H
26 5 ffvelcdmi 
 |-  ( ( A -h ( _i .h B ) ) e. ~H -> ( T ` ( A -h ( _i .h B ) ) ) e. ~H )
27 25 26 ax-mp 
 |-  ( T ` ( A -h ( _i .h B ) ) ) e. ~H
28 23 23 25 27 his35i 
 |-  ( ( _i .h ( A -h ( _i .h B ) ) ) .ih ( _i .h ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( ( _i x. ( * ` _i ) ) x. ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) )
29 23 1 24 hvsubdistr1i 
 |-  ( _i .h ( A -h ( _i .h B ) ) ) = ( ( _i .h A ) -h ( _i .h ( _i .h B ) ) )
30 23 1 hvmulcli 
 |-  ( _i .h A ) e. ~H
31 23 24 hvmulcli 
 |-  ( _i .h ( _i .h B ) ) e. ~H
32 30 31 hvsubvali 
 |-  ( ( _i .h A ) -h ( _i .h ( _i .h B ) ) ) = ( ( _i .h A ) +h ( -u 1 .h ( _i .h ( _i .h B ) ) ) )
33 23 23 2 hvmulassi 
 |-  ( ( _i x. _i ) .h B ) = ( _i .h ( _i .h B ) )
34 33 oveq2i 
 |-  ( -u 1 .h ( ( _i x. _i ) .h B ) ) = ( -u 1 .h ( _i .h ( _i .h B ) ) )
35 ixi 
 |-  ( _i x. _i ) = -u 1
36 35 oveq2i 
 |-  ( -u 1 x. ( _i x. _i ) ) = ( -u 1 x. -u 1 )
37 ax-1cn 
 |-  1 e. CC
38 37 37 mul2negi 
 |-  ( -u 1 x. -u 1 ) = ( 1 x. 1 )
39 1t1e1 
 |-  ( 1 x. 1 ) = 1
40 36 38 39 3eqtri 
 |-  ( -u 1 x. ( _i x. _i ) ) = 1
41 40 oveq1i 
 |-  ( ( -u 1 x. ( _i x. _i ) ) .h B ) = ( 1 .h B )
42 neg1cn 
 |-  -u 1 e. CC
43 23 23 mulcli 
 |-  ( _i x. _i ) e. CC
44 42 43 2 hvmulassi 
 |-  ( ( -u 1 x. ( _i x. _i ) ) .h B ) = ( -u 1 .h ( ( _i x. _i ) .h B ) )
45 ax-hvmulid 
 |-  ( B e. ~H -> ( 1 .h B ) = B )
46 2 45 ax-mp 
 |-  ( 1 .h B ) = B
47 41 44 46 3eqtr3i 
 |-  ( -u 1 .h ( ( _i x. _i ) .h B ) ) = B
48 34 47 eqtr3i 
 |-  ( -u 1 .h ( _i .h ( _i .h B ) ) ) = B
49 48 oveq2i 
 |-  ( ( _i .h A ) +h ( -u 1 .h ( _i .h ( _i .h B ) ) ) ) = ( ( _i .h A ) +h B )
50 32 49 eqtri 
 |-  ( ( _i .h A ) -h ( _i .h ( _i .h B ) ) ) = ( ( _i .h A ) +h B )
51 30 2 hvcomi 
 |-  ( ( _i .h A ) +h B ) = ( B +h ( _i .h A ) )
52 29 50 51 3eqtri 
 |-  ( _i .h ( A -h ( _i .h B ) ) ) = ( B +h ( _i .h A ) )
53 52 fveq2i 
 |-  ( T ` ( _i .h ( A -h ( _i .h B ) ) ) ) = ( T ` ( B +h ( _i .h A ) ) )
54 3 lnopmuli 
 |-  ( ( _i e. CC /\ ( A -h ( _i .h B ) ) e. ~H ) -> ( T ` ( _i .h ( A -h ( _i .h B ) ) ) ) = ( _i .h ( T ` ( A -h ( _i .h B ) ) ) ) )
55 23 25 54 mp2an 
 |-  ( T ` ( _i .h ( A -h ( _i .h B ) ) ) ) = ( _i .h ( T ` ( A -h ( _i .h B ) ) ) )
56 3 lnopaddmuli 
 |-  ( ( _i e. CC /\ B e. ~H /\ A e. ~H ) -> ( T ` ( B +h ( _i .h A ) ) ) = ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) )
57 23 2 1 56 mp3an 
 |-  ( T ` ( B +h ( _i .h A ) ) ) = ( ( T ` B ) +h ( _i .h ( T ` A ) ) )
58 53 55 57 3eqtr3i 
 |-  ( _i .h ( T ` ( A -h ( _i .h B ) ) ) ) = ( ( T ` B ) +h ( _i .h ( T ` A ) ) )
59 52 58 oveq12i 
 |-  ( ( _i .h ( A -h ( _i .h B ) ) ) .ih ( _i .h ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) )
60 cji 
 |-  ( * ` _i ) = -u _i
61 60 oveq2i 
 |-  ( _i x. ( * ` _i ) ) = ( _i x. -u _i )
62 23 23 mulneg2i 
 |-  ( _i x. -u _i ) = -u ( _i x. _i )
63 35 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
64 negneg1e1 
 |-  -u -u 1 = 1
65 63 64 eqtri 
 |-  -u ( _i x. _i ) = 1
66 61 62 65 3eqtri 
 |-  ( _i x. ( * ` _i ) ) = 1
67 66 oveq1i 
 |-  ( ( _i x. ( * ` _i ) ) x. ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( 1 x. ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) )
68 25 1 3 4 lnophmlem1 
 |-  ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) e. RR
69 68 recni 
 |-  ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) e. CC
70 69 mullidi 
 |-  ( 1 x. ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) )
71 67 70 eqtri 
 |-  ( ( _i x. ( * ` _i ) ) x. ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) )
72 28 59 71 3eqtr3i 
 |-  ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) = ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) )
73 23 7 hvmulcli 
 |-  ( _i .h ( T ` A ) ) e. ~H
74 2 30 9 73 hisubcomi 
 |-  ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) = ( ( ( _i .h A ) -h B ) .ih ( ( _i .h ( T ` A ) ) -h ( T ` B ) ) )
75 35 oveq1i 
 |-  ( ( _i x. _i ) .h B ) = ( -u 1 .h B )
76 33 75 eqtr3i 
 |-  ( _i .h ( _i .h B ) ) = ( -u 1 .h B )
77 76 oveq2i 
 |-  ( ( _i .h A ) +h ( _i .h ( _i .h B ) ) ) = ( ( _i .h A ) +h ( -u 1 .h B ) )
78 23 1 24 hvdistr1i 
 |-  ( _i .h ( A +h ( _i .h B ) ) ) = ( ( _i .h A ) +h ( _i .h ( _i .h B ) ) )
79 30 2 hvsubvali 
 |-  ( ( _i .h A ) -h B ) = ( ( _i .h A ) +h ( -u 1 .h B ) )
80 77 78 79 3eqtr4i 
 |-  ( _i .h ( A +h ( _i .h B ) ) ) = ( ( _i .h A ) -h B )
81 80 fveq2i 
 |-  ( T ` ( _i .h ( A +h ( _i .h B ) ) ) ) = ( T ` ( ( _i .h A ) -h B ) )
82 1 24 hvaddcli 
 |-  ( A +h ( _i .h B ) ) e. ~H
83 3 lnopmuli 
 |-  ( ( _i e. CC /\ ( A +h ( _i .h B ) ) e. ~H ) -> ( T ` ( _i .h ( A +h ( _i .h B ) ) ) ) = ( _i .h ( T ` ( A +h ( _i .h B ) ) ) ) )
84 23 82 83 mp2an 
 |-  ( T ` ( _i .h ( A +h ( _i .h B ) ) ) ) = ( _i .h ( T ` ( A +h ( _i .h B ) ) ) )
85 3 lnopmulsubi 
 |-  ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( ( _i .h A ) -h B ) ) = ( ( _i .h ( T ` A ) ) -h ( T ` B ) ) )
86 23 1 2 85 mp3an 
 |-  ( T ` ( ( _i .h A ) -h B ) ) = ( ( _i .h ( T ` A ) ) -h ( T ` B ) )
87 81 84 86 3eqtr3i 
 |-  ( _i .h ( T ` ( A +h ( _i .h B ) ) ) ) = ( ( _i .h ( T ` A ) ) -h ( T ` B ) )
88 80 87 oveq12i 
 |-  ( ( _i .h ( A +h ( _i .h B ) ) ) .ih ( _i .h ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( ( ( _i .h A ) -h B ) .ih ( ( _i .h ( T ` A ) ) -h ( T ` B ) ) )
89 74 88 eqtr4i 
 |-  ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) = ( ( _i .h ( A +h ( _i .h B ) ) ) .ih ( _i .h ( T ` ( A +h ( _i .h B ) ) ) ) )
90 5 ffvelcdmi 
 |-  ( ( A +h ( _i .h B ) ) e. ~H -> ( T ` ( A +h ( _i .h B ) ) ) e. ~H )
91 82 90 ax-mp 
 |-  ( T ` ( A +h ( _i .h B ) ) ) e. ~H
92 23 23 82 91 his35i 
 |-  ( ( _i .h ( A +h ( _i .h B ) ) ) .ih ( _i .h ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( ( _i x. ( * ` _i ) ) x. ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) )
93 66 oveq1i 
 |-  ( ( _i x. ( * ` _i ) ) x. ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( 1 x. ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) )
94 82 1 3 4 lnophmlem1 
 |-  ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) e. RR
95 94 recni 
 |-  ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) e. CC
96 95 mullidi 
 |-  ( 1 x. ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) )
97 93 96 eqtri 
 |-  ( ( _i x. ( * ` _i ) ) x. ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) )
98 89 92 97 3eqtri 
 |-  ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) = ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) )
99 72 98 oveq12i 
 |-  ( ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) - ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) ) = ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) )
100 99 oveq2i 
 |-  ( _i x. ( ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) - ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) ) ) = ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) )
101 22 100 oveq12i 
 |-  ( ( ( ( B +h A ) .ih ( ( T ` B ) +h ( T ` A ) ) ) - ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) ) + ( _i x. ( ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) - ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) )
102 101 oveq1i 
 |-  ( ( ( ( ( B +h A ) .ih ( ( T ` B ) +h ( T ` A ) ) ) - ( ( B -h A ) .ih ( ( T ` B ) -h ( T ` A ) ) ) ) + ( _i x. ( ( ( B +h ( _i .h A ) ) .ih ( ( T ` B ) +h ( _i .h ( T ` A ) ) ) ) - ( ( B -h ( _i .h A ) ) .ih ( ( T ` B ) -h ( _i .h ( T ` A ) ) ) ) ) ) ) / 4 ) = ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) / 4 )
103 10 102 eqtri 
 |-  ( B .ih ( T ` A ) ) = ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) / 4 )
104 103 fveq2i 
 |-  ( * ` ( B .ih ( T ` A ) ) ) = ( * ` ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) / 4 ) )
105 4ne0 
 |-  4 =/= 0
106 1 2 hvaddcli 
 |-  ( A +h B ) e. ~H
107 106 1 3 4 lnophmlem1 
 |-  ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) e. RR
108 1 2 hvsubcli 
 |-  ( A -h B ) e. ~H
109 108 1 3 4 lnophmlem1 
 |-  ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) e. RR
110 107 109 resubcli 
 |-  ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) e. RR
111 110 recni 
 |-  ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) e. CC
112 68 94 resubcli 
 |-  ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) e. RR
113 112 recni 
 |-  ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) e. CC
114 23 113 mulcli 
 |-  ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) e. CC
115 111 114 addcli 
 |-  ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) e. CC
116 4re 
 |-  4 e. RR
117 116 recni 
 |-  4 e. CC
118 115 117 cjdivi 
 |-  ( 4 =/= 0 -> ( * ` ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) / 4 ) ) = ( ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) / ( * ` 4 ) ) )
119 105 118 ax-mp 
 |-  ( * ` ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) / 4 ) ) = ( ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) / ( * ` 4 ) )
120 cjreim 
 |-  ( ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) e. RR /\ ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) e. RR ) -> ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) - ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) )
121 110 112 120 mp2an 
 |-  ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) - ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) )
122 82 2 3 4 lnophmlem1 
 |-  ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) e. RR
123 68 122 resubcli 
 |-  ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) e. RR
124 123 recni 
 |-  ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) e. CC
125 23 124 mulcli 
 |-  ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) e. CC
126 111 125 negsubi 
 |-  ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + -u ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) - ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) )
127 121 126 eqtr4i 
 |-  ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + -u ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) )
128 23 113 mulneg2i 
 |-  ( _i x. -u ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) = -u ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) )
129 69 95 negsubdi2i 
 |-  -u ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) = ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) )
130 129 oveq2i 
 |-  ( _i x. -u ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) = ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) )
131 128 130 eqtr3i 
 |-  -u ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) = ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) )
132 131 oveq2i 
 |-  ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + -u ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) ) )
133 14 oveq2i 
 |-  ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) = ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) )
134 133 20 oveq12i 
 |-  ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) = ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) )
135 3 lnopaddmuli 
 |-  ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( _i .h B ) ) ) = ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) )
136 23 1 2 135 mp3an 
 |-  ( T ` ( A +h ( _i .h B ) ) ) = ( ( T ` A ) +h ( _i .h ( T ` B ) ) )
137 136 oveq2i 
 |-  ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) = ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) )
138 3 lnopsubmuli 
 |-  ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A -h ( _i .h B ) ) ) = ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) )
139 23 1 2 138 mp3an 
 |-  ( T ` ( A -h ( _i .h B ) ) ) = ( ( T ` A ) -h ( _i .h ( T ` B ) ) )
140 139 oveq2i 
 |-  ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) = ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) )
141 137 140 oveq12i 
 |-  ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) = ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) )
142 141 oveq2i 
 |-  ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) ) = ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) )
143 134 142 oveq12i 
 |-  ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) ) )
144 127 132 143 3eqtri 
 |-  ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) = ( ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) ) )
145 cjre 
 |-  ( 4 e. RR -> ( * ` 4 ) = 4 )
146 116 145 ax-mp 
 |-  ( * ` 4 ) = 4
147 144 146 oveq12i 
 |-  ( ( * ` ( ( ( ( A +h B ) .ih ( T ` ( A +h B ) ) ) - ( ( A -h B ) .ih ( T ` ( A -h B ) ) ) ) + ( _i x. ( ( ( A -h ( _i .h B ) ) .ih ( T ` ( A -h ( _i .h B ) ) ) ) - ( ( A +h ( _i .h B ) ) .ih ( T ` ( A +h ( _i .h B ) ) ) ) ) ) ) ) / ( * ` 4 ) ) = ( ( ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) ) ) / 4 )
148 104 119 147 3eqtrri 
 |-  ( ( ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) ) ) / 4 ) = ( * ` ( B .ih ( T ` A ) ) )
149 1 9 2 7 polid2i 
 |-  ( A .ih ( T ` B ) ) = ( ( ( ( ( A +h B ) .ih ( ( T ` A ) +h ( T ` B ) ) ) - ( ( A -h B ) .ih ( ( T ` A ) -h ( T ` B ) ) ) ) + ( _i x. ( ( ( A +h ( _i .h B ) ) .ih ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) ) - ( ( A -h ( _i .h B ) ) .ih ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) ) ) ) ) / 4 )
150 7 2 his1i 
 |-  ( ( T ` A ) .ih B ) = ( * ` ( B .ih ( T ` A ) ) )
151 148 149 150 3eqtr4i 
 |-  ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B )