Metamath Proof Explorer

Theorem lnophmlem2

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

Ref Expression
Hypotheses lnophmlem.1 ⊢ 𝐴 ∈ ℋ
lnophmlem.2 ⊢ 𝐵 ∈ ℋ
lnophmlem.3 ⊢ 𝑇 ∈ LinOp
lnophmlem.4 ⊢ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ
Assertion lnophmlem2 ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 )

Proof

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