Theorem honpcani

Description: Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
	hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
Assertion	honpcani	$$⊢\left(T{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}U=T$$

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
3	1 2 2	hoaddsubi	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=\left(T{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}U$$
4	1 2	hopncani	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=T$$
5	3 4	eqtr3i	$$⊢\left(T{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}U=T$$