# Metamath Proof Explorer

## Theorem hosubid1

Description: The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 ho0sub ${⊢}\left({T}:ℋ⟶ℋ\wedge {0}_{\mathrm{hop}}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)$
3 1 2 mpan2 ${⊢}{T}:ℋ⟶ℋ\to {T}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)$
4 1 hodidi ${⊢}{0}_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}={0}_{\mathrm{hop}}$
5 4 oveq2i ${⊢}{T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)={T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$
6 hoaddid1 ${⊢}{T}:ℋ⟶ℋ\to {T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}$
7 5 6 syl5eq ${⊢}{T}:ℋ⟶ℋ\to {T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)={T}$
8 3 7 eqtrd ${⊢}{T}:ℋ⟶ℋ\to {T}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}$