# Metamath Proof Explorer

## Theorem hosubsub2

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

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 hosubcl ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({T}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
2 honegsub ${⊢}\left({S}:ℋ⟶ℋ\wedge \left({T}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)\right)={S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
3 1 2 sylan2 ${⊢}\left({S}:ℋ⟶ℋ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to {S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)\right)={S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
4 3 3impb ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)\right)={S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
5 honegsubdi2 ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to -1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)={U}{-}_{\mathrm{op}}{T}$
6 5 oveq2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)\right)={S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
7 6 3adant1 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)\right)={S}{+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
8 4 7 eqtr3d ${⊢}\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)$