Theorem hopncani

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

	Ref	Expression
Hypotheses	hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
	hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
Assertion	hopncani	$$⊢\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	hoaddsubassi	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=T{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}U\right)$$
4	2	hodidi	$$⊢U{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
5	4	oveq2i	$$⊢T{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$$
6	1	hoaddid1i	$$⊢T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
7	3 5 6	3eqtri	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=T$$