Theorem hoddii

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

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