Theorem hoaddsubi

Description: Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoaddsubass.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	hoaddsubass.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hoaddsubass.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoaddsubi	$$⊢\left(R{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}T=\left(R{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S$$

Proof

Step	Hyp	Ref	Expression
1		hoaddsubass.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
2		hoaddsubass.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		hoaddsubass.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	1 2	hoaddcomi	$$⊢R{+}_{\mathrm{op}}S=S{+}_{\mathrm{op}}R$$
5	4	oveq1i	$$⊢\left(R{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}T=\left(S{+}_{\mathrm{op}}R\right){-}_{\mathrm{op}}T$$
6	2 1 3	hoaddsubassi	$$⊢\left(S{+}_{\mathrm{op}}R\right){-}_{\mathrm{op}}T=S{+}_{\mathrm{op}}\left(R{-}_{\mathrm{op}}T\right)$$
7	1 3	hosubcli	$$⊢\left(R{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
8	2 7	hoaddcomi	$$⊢S{+}_{\mathrm{op}}\left(R{-}_{\mathrm{op}}T\right)=\left(R{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S$$
9	5 6 8	3eqtri	$$⊢\left(R{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}T=\left(R{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S$$