Theorem hoddi

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

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

Proof

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