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:\mathscr{H}⟶\mathscr{H}$$
Assertion	hodidi	$$⊢T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		hoaddrid.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2	1	hoaddridi	$$⊢T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
3		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
4	1 1 3	hodsi	$$⊢T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}\leftrightarrow T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
5	2 4	mpbir	$$⊢T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}$$