Theorem hosd2i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
3	1 2	hosd1i	$$⊢T{+}_{\mathrm{op}}U=T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
4	2	hodidi	$$⊢U{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
5	4	oveq1i	$$⊢\left(U{-}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=0_{\mathrm{hop}}{-}_{\mathrm{op}}U$$
6	5	oveq2i	$$⊢T{-}_{\mathrm{op}}\left(\left(U{-}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U\right)=T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
7	3 6	eqtr4i	$$⊢T{+}_{\mathrm{op}}U=T{-}_{\mathrm{op}}\left(\left(U{-}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U\right)$$