Theorem hodid

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

	Ref	Expression
Assertion	hodid	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
2	1 1	oveq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to T{-}_{\mathrm{op}}T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
3	2	eqeq1d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}\leftrightarrow if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}\right)$$
4		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
5	4	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
6	5	hodidi	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}$$
7	3 6	dedth	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{-}_{\mathrm{op}}T=0_{\mathrm{hop}}$$