# Metamath Proof Explorer

## Theorem pjddii

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

Ref Expression
Hypotheses pjsdi.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
pjsdi.2 ${⊢}{S}:ℋ⟶ℋ$
pjsdi.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion pjddii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)$

### Proof

Step Hyp Ref Expression
1 pjsdi.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 pjsdi.2 ${⊢}{S}:ℋ⟶ℋ$
3 pjsdi.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 pjsubi ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({T}\left({x}\right)\right)$
7 4 5 6 syl2anc ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\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 {\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({S}{-}_{\mathrm{op}}{T}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\right)$
11 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
12 11 2 hocoi ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right)\right)$
13 11 3 hocoi ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({T}\left({x}\right)\right)$
14 12 13 oveq12d ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right)\left({x}\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({S}\left({x}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({T}\left({x}\right)\right)$
15 7 10 14 3eqtr4d ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({S}{-}_{\mathrm{op}}{T}\right)\left({x}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right)\left({x}\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({x}\right)$
16 2 3 hosubcli ${⊢}\left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
17 11 16 hocoi ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({S}{-}_{\mathrm{op}}{T}\right)\left({x}\right)\right)$
18 11 2 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right):ℋ⟶ℋ$
19 11 3 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right):ℋ⟶ℋ$
20 hodval ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right):ℋ⟶ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right)\left({x}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right)\left({x}\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({x}\right)$
21 18 19 20 mp3an12 ${⊢}{x}\in ℋ\to \left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right)\left({x}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right)\left({x}\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({x}\right)$
22 15 17 21 3eqtr4d ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)\right)\left({x}\right)=\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right)\left({x}\right)$
23 22 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)\right)\left({x}\right)=\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right)\left({x}\right)$
24 11 16 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)\right):ℋ⟶ℋ$
25 18 19 hosubcli ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right):ℋ⟶ℋ$
26 24 25 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)\right)\left({x}\right)=\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\right)\left({x}\right)↔{\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)$
27 23 26 mpbi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({S}{-}_{\mathrm{op}}{T}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {S}\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)$