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

Hypotheses  hosd1.2   T : ~H > ~H 

hosd1.3   U : ~H > ~H 

Assertion  hopncani   ( ( T +op U ) op U ) = T 
Step  Hyp  Ref  Expression 

1  hosd1.2   T : ~H > ~H 

2  hosd1.3   U : ~H > ~H 

3  1 2 2  hoaddsubassi   ( ( T +op U ) op U ) = ( T +op ( U op U ) ) 
4  2  hodidi   ( U op U ) = 0hop 
5  4  oveq2i   ( T +op ( U op U ) ) = ( T +op 0hop ) 
6  1  hoaddid1i   ( T +op 0hop ) = T 
7  3 5 6  3eqtri   ( ( T +op U ) op U ) = T 