# Metamath Proof Explorer

Description: Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to {S}{+}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}$
2 oveq2 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to {T}{+}_{\mathrm{op}}{S}={T}{+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)$
3 1 2 eqeq12d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left({S}{+}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}{S}↔if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)$
4 oveq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
5 oveq1 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {T}{+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)$
6 4 5 eqeq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)↔if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)$
7 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
8 7 elimf ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
9 7 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
10 8 9 hoaddcomi ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)$
11 3 6 10 dedth2h ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}{S}$