# Metamath Proof Explorer

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hosubcl ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
2 hosubsub2 ${⊢}\left(\left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({R}{-}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
3 2 3expb ${⊢}\left(\left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({R}{-}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
4 1 3 sylan ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({R}{-}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
5 hosub4 ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\right)\to \left({R}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
6 5 an42s ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({R}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({U}{-}_{\mathrm{op}}{T}\right)$
7 4 6 eqtr4d ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({R}{-}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({R}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$