Theorem hocsubdiri

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

	Ref	Expression
Hypotheses	hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hocsubdiri	$$⊢\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		hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
2		hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	1 2	hosubcli	$$⊢\left(R{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
5	4 3	hocoi	$$⊢x\in \mathscr{H}\to \left(\left(R{-}_{\mathrm{op}}S\right)\circ T\right)\left(x\right)=\left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)$$
6	1 3	hocofi	$$⊢\left(R\circ T\right):\mathscr{H}⟶\mathscr{H}$$
7	2 3	hocofi	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}$$
8		hodval	$$⊢\left(\left(R\circ T\right):\mathscr{H}⟶\mathscr{H}\wedge \left(S\circ T\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)=\left(R\circ T\right)\left(x\right){-}_{ℎ}\left(S\circ T\right)\left(x\right)$$
9	6 7 8	mp3an12	$$⊢x\in \mathscr{H}\to \left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)=\left(R\circ T\right)\left(x\right){-}_{ℎ}\left(S\circ T\right)\left(x\right)$$
10	3	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
11		hodval	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)=R\left(T\left(x\right)\right){-}_{ℎ}S\left(T\left(x\right)\right)$$
12	1 2 11	mp3an12	$$⊢T\left(x\right)\in \mathscr{H}\to \left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)=R\left(T\left(x\right)\right){-}_{ℎ}S\left(T\left(x\right)\right)$$
13	10 12	syl	$$⊢x\in \mathscr{H}\to \left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)=R\left(T\left(x\right)\right){-}_{ℎ}S\left(T\left(x\right)\right)$$
14	1 3	hocoi	$$⊢x\in \mathscr{H}\to \left(R\circ T\right)\left(x\right)=R\left(T\left(x\right)\right)$$
15	2 3	hocoi	$$⊢x\in \mathscr{H}\to \left(S\circ T\right)\left(x\right)=S\left(T\left(x\right)\right)$$
16	14 15	oveq12d	$$⊢x\in \mathscr{H}\to \left(R\circ T\right)\left(x\right){-}_{ℎ}\left(S\circ T\right)\left(x\right)=R\left(T\left(x\right)\right){-}_{ℎ}S\left(T\left(x\right)\right)$$
17	13 16	eqtr4d	$$⊢x\in \mathscr{H}\to \left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)=\left(R\circ T\right)\left(x\right){-}_{ℎ}\left(S\circ T\right)\left(x\right)$$
18	9 17	eqtr4d	$$⊢x\in \mathscr{H}\to \left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)=\left(R{-}_{\mathrm{op}}S\right)\left(T\left(x\right)\right)$$
19	5 18	eqtr4d	$$⊢x\in \mathscr{H}\to \left(\left(R{-}_{\mathrm{op}}S\right)\circ T\right)\left(x\right)=\left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)$$
20	19	rgen	$$⊢\forall x\in \mathscr{H}\left(\left(R{-}_{\mathrm{op}}S\right)\circ T\right)\left(x\right)=\left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)$$
21	4 3	hocofi	$$⊢\left(\left(R{-}_{\mathrm{op}}S\right)\circ T\right):\mathscr{H}⟶\mathscr{H}$$
22	6 7	hosubcli	$$⊢\left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right):\mathscr{H}⟶\mathscr{H}$$
23	21 22	hoeqi	$$⊢\forall x\in \mathscr{H}\left(\left(R{-}_{\mathrm{op}}S\right)\circ T\right)\left(x\right)=\left(\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)\right)\left(x\right)\leftrightarrow \left(R{-}_{\mathrm{op}}S\right)\circ T=\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)$$
24	20 23	mpbi	$$⊢\left(R{-}_{\mathrm{op}}S\right)\circ T=\left(R\circ T\right){-}_{\mathrm{op}}\left(S\circ T\right)$$