Theorem pjsdii

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

	Ref	Expression
Hypotheses	pjsdi.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjsdi.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	pjsdi.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	pjsdii	$$⊢{\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}}_{\mathscr{H}}$$
2		pjsdi.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		pjsdi.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	2	ffvelcdmi	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
5	3	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
6	1	pjaddi	$$⊢\left(S\left(x\right)\in \mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\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 \mathscr{H}\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		hosval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\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 \mathscr{H}\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
10	9	fveq2d	$$⊢x\in \mathscr{H}\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):\mathscr{H}⟶\mathscr{H}$$
12	11 2	hocoi	$$⊢x\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
17	11 16	hocoi	$$⊢x\in \mathscr{H}\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):\mathscr{H}⟶\mathscr{H}$$
19	11 3	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right):\mathscr{H}⟶\mathscr{H}$$
20		hosval	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ S\right):\mathscr{H}⟶\mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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):\mathscr{H}⟶\mathscr{H}$$
25	18 19	hoaddcli	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ S\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right)\right):\mathscr{H}⟶\mathscr{H}$$
26	24 25	hoeqi	$$⊢\forall x\in \mathscr{H}\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)\leftrightarrow {\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)$$