Theorem hoaddsubassi

Description: Associativity of 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	hoaddsubassi	$$⊢\left(R{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}T\right)$$

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		hoaddsubass	$$⊢\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){-}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}T\right)$$
5	1 2 3 4	mp3an	$$⊢\left(R{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}T\right)$$