# Metamath Proof Explorer

## Theorem ho0sub

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion ho0sub ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to {S}{-}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{T}$
2 oveq1 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to {S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)$
3 1 2 eqeq12d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left({S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)↔if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)$
4 oveq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
5 oveq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}={0}_{\mathrm{hop}}{-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
6 5 oveq2d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
7 4 6 eqeq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)↔if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)\right)$
8 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
9 8 elimf ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
10 8 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
11 9 10 ho0subi ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
12 3 7 11 dedth2h ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)$