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}}_{\mathscr{H}}$$
	pjsdi2.2	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	pjsdi2.3	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	pjsdi2.4	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
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}}_{\mathscr{H}}$$
2		pjsdi2.2	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
3		pjsdi2.3	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
4		pjsdi2.4	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
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):\mathscr{H}⟶\mathscr{H}$$
7	2 4	hocofi	$$⊢\left(R\circ T\right):\mathscr{H}⟶\mathscr{H}$$
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	eqtrdi	$$⊢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)$$