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	|- T : ~H --> ~H
Assertion	hodidi	|- ( T -op T ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		hoaddrid.1	|- T : ~H --> ~H
2	1	hoaddridi	|- ( 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