Metamath Proof Explorer

Theorem lnopunilem1

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

Ref Expression
Hypotheses lnopunilem.1 ⊢ T ∈ LinOp
lnopunilem.2 ⊢ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x
lnopunilem.3 ⊢ A ∈ ℋ
lnopunilem.4 ⊢ B ∈ ℋ
lnopunilem1.5 ⊢ C ∈ ℂ
Assertion lnopunilem1 ⊢ ℜ ⁡ C ⁢ T ⁡ A ⋅ ih T ⁡ B = ℜ ⁡ C ⁢ A ⋅ ih B

Proof

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