# Metamath Proof Explorer

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

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

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to {R}{+}_{\mathrm{op}}{S}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}$
2 1 oveq1d ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to \left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}$
3 oveq1 ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to {R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$
4 2 3 eqeq12d ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)$
5 oveq2 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)$
6 5 oveq1d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}{T}$
7 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}$
8 7 oveq2d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}\right)$
9 6 8 eqeq12d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left(\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}{T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}\right)\right)$
10 oveq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}{T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
11 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)$
12 11 oveq2d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}\right)=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
13 10 12 eqeq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left(\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}{T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)\right)$
14 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
15 14 elimf ${⊢}if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
16 14 elimf ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
17 14 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
18 15 16 17 hoaddassi ${⊢}\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
19 4 9 13 18 dedth3h ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$