# Metamath Proof Explorer

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

Ref Expression
Assertion hoadd4 ${⊢}\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}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$

### Proof

Step Hyp Ref Expression
1 hoadd32 ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$
2 1 oveq1d ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}$
3 2 3expa ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge {T}:ℋ⟶ℋ\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}$
4 3 adantrr ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}$
5 hoaddcl ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left({R}{+}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
6 hoaddass ${⊢}\left(\left({R}{+}_{\mathrm{op}}{S}\right):ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)$
7 6 3expb ${⊢}\left(\left({R}{+}_{\mathrm{op}}{S}\right):ℋ⟶ℋ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)$
8 5 7 sylan ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)$
9 hoaddcl ${⊢}\left({R}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({R}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
10 hoaddass ${⊢}\left(\left({R}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$
11 10 3expb ${⊢}\left(\left({R}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$
12 9 11 sylan ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({S}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$
13 12 an4s ${⊢}\left(\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{U}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$
14 4 8 13 3eqtr3d ${⊢}\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}}{T}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{U}\right)$