# Metamath Proof Explorer

Description: Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses hoaddsubass.1 ${⊢}{R}:ℋ⟶ℋ$
hoaddsubass.2 ${⊢}{S}:ℋ⟶ℋ$
hoaddsubass.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion hoaddsubi ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}{T}=\left({R}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$

### Proof

Step Hyp Ref Expression
1 hoaddsubass.1 ${⊢}{R}:ℋ⟶ℋ$
2 hoaddsubass.2 ${⊢}{S}:ℋ⟶ℋ$
3 hoaddsubass.3 ${⊢}{T}:ℋ⟶ℋ$
4 1 2 hoaddcomi ${⊢}{R}{+}_{\mathrm{op}}{S}={S}{+}_{\mathrm{op}}{R}$
5 4 oveq1i ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}{T}=\left({S}{+}_{\mathrm{op}}{R}\right){-}_{\mathrm{op}}{T}$
6 2 1 3 hoaddsubassi ${⊢}\left({S}{+}_{\mathrm{op}}{R}\right){-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({R}{-}_{\mathrm{op}}{T}\right)$
7 1 3 hosubcli ${⊢}\left({R}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
8 2 7 hoaddcomi ${⊢}{S}{+}_{\mathrm{op}}\left({R}{-}_{\mathrm{op}}{T}\right)=\left({R}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$
9 5 6 8 3eqtri ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}{T}=\left({R}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$