# Metamath Proof Explorer

## Theorem hocsubdiri

Description: Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hods.1 ${⊢}{R}:ℋ⟶ℋ$
hods.2 ${⊢}{S}:ℋ⟶ℋ$
hods.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion hocsubdiri ${⊢}\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 hods.1 ${⊢}{R}:ℋ⟶ℋ$
2 hods.2 ${⊢}{S}:ℋ⟶ℋ$
3 hods.3 ${⊢}{T}:ℋ⟶ℋ$
4 1 2 hosubcli ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
5 4 3 hocoi ${⊢}{x}\in ℋ\to \left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}\right)\left({x}\right)=\left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)$
6 1 3 hocofi ${⊢}\left({R}\circ {T}\right):ℋ⟶ℋ$
7 2 3 hocofi ${⊢}\left({S}\circ {T}\right):ℋ⟶ℋ$
8 hodval ${⊢}\left(\left({R}\circ {T}\right):ℋ⟶ℋ\wedge \left({S}\circ {T}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)=\left({R}\circ {T}\right)\left({x}\right){-}_{ℎ}\left({S}\circ {T}\right)\left({x}\right)$
9 6 7 8 mp3an12 ${⊢}{x}\in ℋ\to \left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)=\left({R}\circ {T}\right)\left({x}\right){-}_{ℎ}\left({S}\circ {T}\right)\left({x}\right)$
10 3 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
11 hodval ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to \left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)={R}\left({T}\left({x}\right)\right){-}_{ℎ}{S}\left({T}\left({x}\right)\right)$
12 1 2 11 mp3an12 ${⊢}{T}\left({x}\right)\in ℋ\to \left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)={R}\left({T}\left({x}\right)\right){-}_{ℎ}{S}\left({T}\left({x}\right)\right)$
13 10 12 syl ${⊢}{x}\in ℋ\to \left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)={R}\left({T}\left({x}\right)\right){-}_{ℎ}{S}\left({T}\left({x}\right)\right)$
14 1 3 hocoi ${⊢}{x}\in ℋ\to \left({R}\circ {T}\right)\left({x}\right)={R}\left({T}\left({x}\right)\right)$
15 2 3 hocoi ${⊢}{x}\in ℋ\to \left({S}\circ {T}\right)\left({x}\right)={S}\left({T}\left({x}\right)\right)$
16 14 15 oveq12d ${⊢}{x}\in ℋ\to \left({R}\circ {T}\right)\left({x}\right){-}_{ℎ}\left({S}\circ {T}\right)\left({x}\right)={R}\left({T}\left({x}\right)\right){-}_{ℎ}{S}\left({T}\left({x}\right)\right)$
17 13 16 eqtr4d ${⊢}{x}\in ℋ\to \left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)=\left({R}\circ {T}\right)\left({x}\right){-}_{ℎ}\left({S}\circ {T}\right)\left({x}\right)$
18 9 17 eqtr4d ${⊢}{x}\in ℋ\to \left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)=\left({R}{-}_{\mathrm{op}}{S}\right)\left({T}\left({x}\right)\right)$
19 5 18 eqtr4d ${⊢}{x}\in ℋ\to \left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}\right)\left({x}\right)=\left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)$
20 19 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}\right)\left({x}\right)=\left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)$
21 4 3 hocofi ${⊢}\left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}\right):ℋ⟶ℋ$
22 6 7 hosubcli ${⊢}\left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right):ℋ⟶ℋ$
23 21 22 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}\right)\left({x}\right)=\left(\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)\right)\left({x}\right)↔\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)$
24 20 23 mpbi ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right)\circ {T}=\left({R}\circ {T}\right){-}_{\mathrm{op}}\left({S}\circ {T}\right)$