# Metamath Proof Explorer

Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hods.1 ${⊢}{R}:ℋ⟶ℋ$
hods.2 ${⊢}{S}:ℋ⟶ℋ$
hods.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion hoadd32i ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$

### Proof

Step Hyp Ref Expression
1 hods.1 ${⊢}{R}:ℋ⟶ℋ$
2 hods.2 ${⊢}{S}:ℋ⟶ℋ$
3 hods.3 ${⊢}{T}:ℋ⟶ℋ$
4 2 3 hoaddcomi ${⊢}{S}{+}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}{S}$
5 4 oveq2i ${⊢}{R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)={R}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{S}\right)$
6 1 2 3 hoaddassi ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$
7 1 3 2 hoaddassi ${⊢}\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}={R}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{S}\right)$
8 5 6 7 3eqtr4i ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=\left({R}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}{S}$