# Metamath Proof Explorer

## Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegsub ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{-}_{\mathrm{op}}{U}$

### Proof

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