Metamath Proof Explorer

Theorem lnopunilem1

Description: Lemma for lnopunii . (Contributed by NM, 14-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses lnopunilem.1 ⊢ 𝑇 ∈ LinOp
lnopunilem.2 ⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
lnopunilem.3 ⊢ 𝐴 ∈ ℋ
lnopunilem.4 ⊢ 𝐵 ∈ ℋ
lnopunilem1.5 ⊢ 𝐶 ∈ ℂ
Assertion lnopunilem1 ( ℜ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lnopunilem.1 ⊢ 𝑇 ∈ LinOp
2 lnopunilem.2 ⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
3 lnopunilem.3 ⊢ 𝐴 ∈ ℋ
4 lnopunilem.4 ⊢ 𝐵 ∈ ℋ
5 lnopunilem1.5 ⊢ 𝐶 ∈ ℂ
6 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
7 6 ffvelrni ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
8 3 7 ax-mp ⊢ ( 𝑇 ‘ 𝐴 ) ∈ ℋ
9 6 ffvelrni ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℋ )
10 4 9 ax-mp ⊢ ( 𝑇 ‘ 𝐵 ) ∈ ℋ
11 8 10 hicli ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ
12 5 11 mulcli ⊢ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ∈ ℂ
13 reval ⊢ ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ∈ ℂ → ( ℜ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) / 2 ) )
14 12 13 ax-mp ⊢ ( ℜ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) / 2 )
15 3 4 hicli ⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
16 5 15 mulcli ⊢ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ∈ ℂ
17 reval ⊢ ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ∈ ℂ → ( ℜ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) / 2 ) )
18 16 17 ax-mp ⊢ ( ℜ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) / 2 )
19 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) )
20 fveq2 ⊢ ( 𝑥 = 𝑦 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝑦 ) )
21 19 20 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) ) )
22 21 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) )
23 2 22 mpbi ⊢ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 )
24 oveq1 ⊢ ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↑ 2 ) = ( ( normℎ ‘ 𝑦 ) ↑ 2 ) )
25 6 ffvelrni ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
26 normsq ⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↑ 2 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
27 25 26 syl ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↑ 2 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
28 normsq ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ↑ 2 ) = ( 𝑦 ·ih 𝑦 ) )
29 27 28 eqeq12d ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ↑ 2 ) = ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ↔ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) ) )
30 24 29 syl5ib ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) → ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) ) )
31 30 ralimia ⊢ ( ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) → ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) )
32 23 31 ax-mp ⊢ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 )
33 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝐴 ) )
34 33 33 oveq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
35 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
36 35 35 oveq12d ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ·ih 𝑦 ) = ( 𝐴 ·ih 𝐴 ) )
37 34 36 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( 𝐴 ·ih 𝐴 ) ) )
38 37 rspcv ⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) → ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( 𝐴 ·ih 𝐴 ) ) )
39 3 32 38 mp2 ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( 𝐴 ·ih 𝐴 )
40 39 oveq2i ⊢ ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) )
41 40 oveq2i ⊢ ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) = ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) )
42 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝐵 ) )
43 42 42 oveq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
44 id ⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
45 44 44 oveq12d ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ·ih 𝑦 ) = ( 𝐵 ·ih 𝐵 ) )
46 43 45 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐵 ·ih 𝐵 ) ) )
47 46 rspcv ⊢ ( 𝐵 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) → ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐵 ·ih 𝐵 ) ) )
48 4 32 47 mp2 ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐵 ·ih 𝐵 )
49 41 48 oveq12i ⊢ ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) = ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) )
50 49 oveq1i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) )
51 5 cjcli ⊢ ( ∗ ‘ 𝐶 ) ∈ ℂ
52 8 8 hicli ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℂ
53 51 52 mulcli ⊢ ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ∈ ℂ
54 5 53 mulcli ⊢ ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) ∈ ℂ
55 10 10 hicli ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ
56 12 cjcli ⊢ ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ∈ ℂ
57 54 55 12 56 add42i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
58 3 3 hicli ⊢ ( 𝐴 ·ih 𝐴 ) ∈ ℂ
59 51 58 mulcli ⊢ ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ∈ ℂ
60 5 59 mulcli ⊢ ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) ∈ ℂ
61 4 4 hicli ⊢ ( 𝐵 ·ih 𝐵 ) ∈ ℂ
62 16 cjcli ⊢ ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ
63 60 61 16 62 add42i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) )
64 5 3 hvmulcli ⊢ ( 𝐶 ·ℎ 𝐴 ) ∈ ℋ
65 64 4 hvaddcli ⊢ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ∈ ℋ
66 fveq2 ⊢ ( 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) )
67 66 66 oveq12d ⊢ ( 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) → ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) )
68 id ⊢ ( 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) → 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) )
69 68 68 oveq12d ⊢ ( 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) → ( 𝑦 ·ih 𝑦 ) = ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) )
70 67 69 eqeq12d ⊢ ( 𝑦 = ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) → ( ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) )
71 70 rspcv ⊢ ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑦 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) → ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) )
72 65 32 71 mp2 ⊢ ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) )
73 ax-his2 ⊢ ( ( ( 𝐶 ·ℎ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ∈ ℋ ) → ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) + ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) )
74 64 4 65 73 mp3an ⊢ ( ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) + ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) )
75 ax-his3 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) )
76 5 3 65 75 mp3an ⊢ ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) )
77 his7 ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐶 ·ℎ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐴 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) ) )
78 3 64 4 77 mp3an ⊢ ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐴 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) )
79 his5 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ·ih ( 𝐶 ·ℎ 𝐴 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) )
80 5 3 3 79 mp3an ⊢ ( 𝐴 ·ih ( 𝐶 ·ℎ 𝐴 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) )
81 80 oveq1i ⊢ ( ( 𝐴 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) ) = ( ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) )
82 78 81 eqtri ⊢ ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) )
83 82 oveq2i ⊢ ( 𝐶 · ( 𝐴 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( 𝐶 · ( ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) ) )
84 5 59 15 adddii ⊢ ( 𝐶 · ( ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) + ( 𝐴 ·ih 𝐵 ) ) ) = ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
85 76 83 84 3eqtri ⊢ ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
86 his7 ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ·ℎ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐵 ·ih 𝐵 ) ) )
87 4 64 4 86 mp3an ⊢ ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐵 ·ih 𝐵 ) )
88 his5 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 ·ih 𝐴 ) ) )
89 5 4 3 88 mp3an ⊢ ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 ·ih 𝐴 ) )
90 5 15 cjmuli ⊢ ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) )
91 4 3 his1i ⊢ ( 𝐵 ·ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) )
92 91 oveq2i ⊢ ( ( ∗ ‘ 𝐶 ) · ( 𝐵 ·ih 𝐴 ) ) = ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ ( 𝐴 ·ih 𝐵 ) ) )
93 90 92 eqtr4i ⊢ ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝐵 ·ih 𝐴 ) )
94 89 93 eqtr4i ⊢ ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) = ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
95 94 oveq1i ⊢ ( ( 𝐵 ·ih ( 𝐶 ·ℎ 𝐴 ) ) + ( 𝐵 ·ih 𝐵 ) ) = ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) )
96 87 95 eqtri ⊢ ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) )
97 85 96 oveq12i ⊢ ( ( ( 𝐶 ·ℎ 𝐴 ) ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) + ( 𝐵 ·ih ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) )
98 72 74 97 3eqtrri ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) ) = ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) )
99 1 lnopli ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) )
100 5 3 4 99 mp3an ⊢ ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) = ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) )
101 100 100 oveq12i ⊢ ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) )
102 5 8 hvmulcli ⊢ ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ∈ ℋ
103 102 10 hvaddcli ⊢ ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ∈ ℋ
104 ax-his2 ⊢ ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℋ ∧ ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ∈ ℋ ) → ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) ) )
105 102 10 103 104 mp3an ⊢ ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
106 101 105 eqtri ⊢ ( ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ·ih ( 𝑇 ‘ ( ( 𝐶 ·ℎ 𝐴 ) +ℎ 𝐵 ) ) ) = ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
107 ax-his3 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ∈ ℋ ) → ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) ) )
108 5 8 103 107 mp3an ⊢ ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
109 his7 ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
110 8 102 10 109 mp3an ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
111 his5 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) )
112 5 8 8 111 mp3an ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
113 112 oveq1i ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
114 110 113 eqtri ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
115 114 oveq2i ⊢ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) ) = ( 𝐶 · ( ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
116 5 53 11 adddii ⊢ ( 𝐶 · ( ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
117 108 115 116 3eqtri ⊢ ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
118 his7 ⊢ ( ( ( 𝑇 ‘ 𝐵 ) ∈ ℋ ∧ ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
119 10 102 10 118 mp3an ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
120 his5 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) )
121 5 10 8 120 mp3an ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
122 5 11 cjmuli ⊢ ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
123 10 8 his1i ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
124 123 oveq2i ⊢ ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
125 122 124 eqtr4i ⊢ ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
126 121 125 eqtr4i ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
127 126 oveq1i ⊢ ( ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
128 119 127 eqtri ⊢ ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) = ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) )
129 117 128 oveq12i ⊢ ( ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( ( 𝐶 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
130 98 106 129 3eqtrri ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) )
131 63 130 eqtr4i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) )
132 57 131 eqtr4i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) ) ) + ( ( 𝑇 ‘ 𝐵 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) )
133 50 132 eqtr3i ⊢ ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) )
134 60 61 addcli ⊢ ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) ∈ ℂ
135 12 56 addcli ⊢ ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ∈ ℂ
136 16 62 addcli ⊢ ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) ∈ ℂ
137 134 135 136 addcani ⊢ ( ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) ) = ( ( ( 𝐶 · ( ( ∗ ‘ 𝐶 ) · ( 𝐴 ·ih 𝐴 ) ) ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) ) ↔ ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) = ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) )
138 133 137 mpbi ⊢ ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) = ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) )
139 138 oveq1i ⊢ ( ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) / 2 ) = ( ( ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) + ( ∗ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) ) / 2 )
140 18 139 eqtr4i ⊢ ( ℜ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) + ( ∗ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) ) / 2 )
141 14 140 eqtr4i ⊢ ( ℜ ‘ ( 𝐶 · ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐵 ) ) ) ) = ( ℜ ‘ ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )