Theorem hodseqi

Description: Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hodseq.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hodseq.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3		eqid	$$⊢T{-}_{\mathrm{op}}S=T{-}_{\mathrm{op}}S$$
4	2 1	hosubcli	$$⊢\left(T{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
5	2 1 4	hodsi	$$⊢T{-}_{\mathrm{op}}S=T{-}_{\mathrm{op}}S\leftrightarrow S{+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}S\right)=T$$
6	3 5	mpbi	$$⊢S{+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}S\right)=T$$