Metamath Proof Explorer

Theorem hodidi

Description: Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddid1.1 
|- T : ~H --> ~H
Assertion hodidi 
|- ( T -op T ) = 0hop

Proof

Step Hyp Ref Expression
1 hoaddid1.1 
 |-  T : ~H --> ~H
2 1 hoaddid1i 
 |-  ( T +op 0hop ) = T
3 ho0f 
 |-  0hop : ~H --> ~H
4 1 1 3 hodsi 
 |-  ( ( T -op T ) = 0hop <-> ( T +op 0hop ) = T )
5 2 4 mpbir 
 |-  ( T -op T ) = 0hop