Theorem hocsubdir

Description: Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hocsubdir	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right)\circ T=\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to R{-}_{\mathrm{op}}S=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S$$
2	1	coeq1d	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to \left(R{-}_{\mathrm{op}}S\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S\right)\circ T$$
3		coeq1	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to R\circ T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T$$
4	3	oveq1d	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to \left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)$$
5	2 4	eqeq12d	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to \left(\left(R{-}_{\mathrm{op}}S\right)\circ T=\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)$$
6		oveq2	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)$$
7	6	coeq1d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ T$$
8		coeq1	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to S\circ T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T$$
9	8	oveq2d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T\right)$$
10	7 9	eqeq12d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}S\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T\right)\right)$$
11		coeq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
12		coeq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
13		coeq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
14	12 13	oveq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T\right)=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
15	11 14	eqeq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ T\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)\right)$$
16		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
17	16	elimf	$$⊢if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
18	16	elimf	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
19	16	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
20	17 18 19	hocsubdiri	$$⊢\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right){-}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\circ if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
21	5 10 15 20	dedth3h	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right)\circ T=\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)$$