# Metamath Proof Explorer

## Theorem hocsubdir

Description: Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hocsubdir ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {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 coeq1d ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to \left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{S}\right)\circ {T}$
3 coeq1 ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to {R}\circ {T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}$
4 3 oveq1d ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to \left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)$
5 2 4 eqeq12d ${⊢}{R}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\to \left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{S}\right)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)$
6 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)$
7 6 coeq1d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{S}\right)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)\circ {T}$
8 coeq1 ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to {S}\circ {T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}$
9 8 oveq2d ${⊢}{S}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\to \left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}\right)$
10 7 9 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)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}\right)\right)$
11 coeq2 ${⊢}{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)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
12 coeq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}=if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
13 coeq2 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}=if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
14 12 13 oveq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}\right)=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
15 11 14 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)\circ {T}=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ {T}\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ {T}\right)↔\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)\right)$
16 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
17 16 elimf ${⊢}if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
18 16 elimf ${⊢}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
19 16 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
20 17 18 19 hocsubdiri ${⊢}\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)=\left(if\left({R}:ℋ⟶ℋ,{R},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left({S}:ℋ⟶ℋ,{S},{0}_{\mathrm{hop}}\right)\circ if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
21 5 10 15 20 dedth3h ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)$