# Metamath Proof Explorer

## Theorem hosd2i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
Assertion hosd2i ${⊢}{T}{+}_{\mathrm{op}}{U}={T}{-}_{\mathrm{op}}\left(\left({U}{-}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}\right)$

### Proof

Step Hyp Ref Expression
1 hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
2 hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
3 1 2 hosd1i ${⊢}{T}{+}_{\mathrm{op}}{U}={T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
4 2 hodidi ${⊢}{U}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}$
5 4 oveq1i ${⊢}\left({U}{-}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}$
6 5 oveq2i ${⊢}{T}{-}_{\mathrm{op}}\left(\left({U}{-}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}\right)={T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
7 3 6 eqtr4i ${⊢}{T}{+}_{\mathrm{op}}{U}={T}{-}_{\mathrm{op}}\left(\left({U}{-}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}\right)$