# Metamath Proof Explorer

## Theorem hosubsub

Description: Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubsub ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}$

### Proof

Step Hyp Ref Expression
1 hosubsub2 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)={S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
2 hoaddsubass ${⊢}\left({S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{T}={S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
3 hoaddsub ${⊢}\left({S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{T}=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}$
4 2 3 eqtr3d ${⊢}\left({S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}$
5 4 3com23 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}$
6 1 5 eqtrd ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}$