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 : ~H --> ~H
	hodseq.3	|- T : ~H --> ~H
Assertion	hodseqi	|- ( S +op ( T -op S ) ) = T

Proof

Step	Hyp	Ref	Expression
1		hodseq.2	|- S : ~H --> ~H
2		hodseq.3	|- T : ~H --> ~H
3		eqid	|- ( T -op S ) = ( T -op S )
4	2 1	hosubcli	|- ( T -op S ) : ~H --> ~H
5	2 1 4	hodsi	|- ( ( T -op S ) = ( T -op S ) <-> ( S +op ( T -op S ) ) = T )
6	3 5	mpbi	|- ( S +op ( T -op S ) ) = T