Description: Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27Aug2004) (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 
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 