# Metamath Proof Explorer

## Theorem hoddi

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoddi ${⊢}\left({R}\in \mathrm{LinOp}\wedge {S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {R}\circ \left({S}{-}_{\mathrm{op}}{T}\right)=\left({R}\circ {S}\right){-}_{\mathrm{op}}\left({R}\circ {T}\right)$

### Proof

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