# Metamath Proof Explorer

## Theorem ho0subi

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

Ref Expression
Hypotheses hodseq.2 ${⊢}{S}:ℋ⟶ℋ$
hodseq.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion ho0subi ${⊢}{S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)$

### Proof

Step Hyp Ref Expression
1 hodseq.2 ${⊢}{S}:ℋ⟶ℋ$
2 hodseq.3 ${⊢}{T}:ℋ⟶ℋ$
3 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
4 3 2 hosubcli ${⊢}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
5 2 1 4 hoadd12i ${⊢}{T}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)={S}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)$
6 2 3 hodseqi ${⊢}{T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)={0}_{\mathrm{hop}}$
7 6 oveq2i ${⊢}{S}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)={S}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$
8 1 hoaddid1i ${⊢}{S}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={S}$
9 5 7 8 3eqtri ${⊢}{T}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)={S}$
10 1 4 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right):ℋ⟶ℋ$
11 1 2 10 hodsi ${⊢}{S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)↔{T}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)\right)={S}$
12 9 11 mpbir ${⊢}{S}{-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{T}\right)$