# 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}\in \mathrm{LinOp}$
lnopunilem.2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)$
lnopunilem.3 ${⊢}{A}\in ℋ$
lnopunilem.4 ${⊢}{B}\in ℋ$
lnopunilem1.5 ${⊢}{C}\in ℂ$
Assertion lnopunilem1 ${⊢}\Re \left({C}\left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)\right)\right)=\Re \left({C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$

### Proof

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