# Metamath Proof Explorer

## Theorem lnopeq0lem2

Description: Lemma for lnopeq0i . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopeq0.1 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopeq0lem2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$

### Proof

Step Hyp Ref Expression
1 lnopeq0.1 ${⊢}{T}\in \mathrm{LinOp}$
2 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
3 2 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}$
4 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{+}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)$
5 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{+}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}$
6 4 5 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)$
7 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)$
8 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{-}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}$
9 7 8 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)$
10 6 9 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)$
11 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
12 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)$
13 11 12 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
14 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
15 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)$
16 14 15 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
17 13 16 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)$
18 17 oveq2d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)$
19 10 18 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)$
20 19 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$
21 3 20 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}↔{T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}\right)$
22 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
23 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
24 23 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
25 24 23 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
26 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
27 26 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
28 27 26 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
29 25 28 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
30 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \mathrm{i}{\cdot }_{ℎ}{B}=\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
31 30 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
32 31 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
33 32 31 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
34 30 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
35 34 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
36 35 34 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
37 33 36 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)$
38 37 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)\right)$
39 29 38 oveq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)\right)$
40 39 oveq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)\right)}{4}$
41 22 40 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}↔{T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)\right)}{4}\right)$
42 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
43 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
44 1 42 43 lnopeq0lem1 ${⊢}{T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=\frac{\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)+\mathrm{i}\left(\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)-\left({T}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)\right)\right)}{4}$
45 21 41 44 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$