Description: Hilbert space operator cancellation law. (Contributed by NM, 11Mar2006) (New usage is discouraged.)
Ref  Expression  

Hypotheses  honpncan.1   R : ~H > ~H 

honpncan.2   S : ~H > ~H 

honpncan.3   T : ~H > ~H 

Assertion  honpncani   ( ( R op S ) +op ( S op T ) ) = ( R op T ) 
Step  Hyp  Ref  Expression 

1  honpncan.1   R : ~H > ~H 

2  honpncan.2   S : ~H > ~H 

3  honpncan.3   T : ~H > ~H 

4  1 2  hosubcli   ( R op S ) : ~H > ~H 
5  4 2 3  hoaddsubassi   ( ( ( R op S ) +op S ) op T ) = ( ( R op S ) +op ( S op T ) ) 
6  1 2  honpcani   ( ( R op S ) +op S ) = R 
7  6  oveq1i   ( ( ( R op S ) +op S ) op T ) = ( R op T ) 
8  5 7  eqtr3i   ( ( R op S ) +op ( S op T ) ) = ( R op T ) 