# Metamath Proof Explorer

Description: Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

### Proof

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