# Metamath Proof Explorer

## Theorem hodid

Description: Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hodid ${⊢}{T}:ℋ⟶ℋ\to {T}{-}_{\mathrm{op}}{T}={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
2 1 1 oveq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {T}{-}_{\mathrm{op}}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
3 2 eqeq1d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left({T}{-}_{\mathrm{op}}{T}={0}_{\mathrm{hop}}↔if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)={0}_{\mathrm{hop}}\right)$
4 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
5 4 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
6 5 hodidi ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)={0}_{\mathrm{hop}}$
7 3 6 dedth ${⊢}{T}:ℋ⟶ℋ\to {T}{-}_{\mathrm{op}}{T}={0}_{\mathrm{hop}}$