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 hoaddrid.1 𝑇 : ℋ ⟶ ℋ
Assertion hodidi ( 𝑇op 𝑇 ) = 0hop

Proof

Step Hyp Ref Expression
1 hoaddrid.1 𝑇 : ℋ ⟶ ℋ
2 1 hoaddridi ( 𝑇 +op 0hop ) = 𝑇
3 ho0f 0hop : ℋ ⟶ ℋ
4 1 1 3 hodsi ( ( 𝑇op 𝑇 ) = 0hop ↔ ( 𝑇 +op 0hop ) = 𝑇 )
5 2 4 mpbir ( 𝑇op 𝑇 ) = 0hop