# Metamath Proof Explorer

## Theorem pjsdi2i

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

Ref Expression
Hypotheses pjsdi2.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
pjsdi2.2 ${⊢}{R}:ℋ⟶ℋ$
pjsdi2.3 ${⊢}{S}:ℋ⟶ℋ$
pjsdi2.4 ${⊢}{T}:ℋ⟶ℋ$
Assertion pjsdi2i ${⊢}{R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {S}\right){+}_{\mathrm{op}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {T}\right)$

### Proof

Step Hyp Ref Expression
1 pjsdi2.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 pjsdi2.2 ${⊢}{R}:ℋ⟶ℋ$
3 pjsdi2.3 ${⊢}{S}:ℋ⟶ℋ$
4 pjsdi2.4 ${⊢}{T}:ℋ⟶ℋ$
5 coeq2 ${⊢}{R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left(\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\right)$
6 2 3 hocofi ${⊢}\left({R}\circ {S}\right):ℋ⟶ℋ$
7 2 4 hocofi ${⊢}\left({R}\circ {T}\right):ℋ⟶ℋ$
8 1 6 7 pjsdii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left(\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {S}\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {T}\right)\right)$
9 5 8 syl6eq ${⊢}{R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {S}\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {T}\right)\right)$
10 coass ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ \left({S}{+}_{\mathrm{op}}{T}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)\right)$
11 coass ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {S}={\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {S}\right)$
12 coass ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {T}={\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {T}\right)$
13 11 12 oveq12i ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {S}\right){+}_{\mathrm{op}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {T}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {S}\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({R}\circ {T}\right)\right)$
14 9 10 13 3eqtr4g ${⊢}{R}\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left({R}\circ {S}\right){+}_{\mathrm{op}}\left({R}\circ {T}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ \left({S}{+}_{\mathrm{op}}{T}\right)=\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {S}\right){+}_{\mathrm{op}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {R}\right)\circ {T}\right)$