# Metamath Proof Explorer

## Theorem hosubsub4

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

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

### Proof

Step Hyp Ref Expression
1 neg1cn ${⊢}-1\in ℂ$
2 homulcl ${⊢}\left(-1\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
3 1 2 mpan ${⊢}{U}:ℋ⟶ℋ\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
4 hosubsub ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)$
5 3 4 syl3an3 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)$
6 hosubneg ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}$
7 6 3adant1 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}$
8 7 oveq2d ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={S}{-}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)$
9 hosubcl ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
10 honegsub ${⊢}\left(\left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}$
11 9 10 stoic3 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{-}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)=\left({S}{-}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}$
12 5 8 11 3eqtr3rd ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{-}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}={S}{-}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)$