# Metamath Proof Explorer

## Theorem hoddii

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

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