Theorem hosubid1

Description: The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
2		ho0sub	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge 0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\right)\to T{-}_{\mathrm{op}}{0}_{\mathrm{hop}}=T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)$$
3	1 2	mpan2	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{-}_{\mathrm{op}}{0}_{\mathrm{hop}}=T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)$$
4	1	hodidi	$$⊢0_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}=0_{\mathrm{hop}}$$
5	4	oveq2i	$$⊢T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)=T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$$
6		hoaddid1	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
7	5 6	syl5eq	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)=T$$
8	3 7	eqtrd	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T{-}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$