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

Proof

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