Theorem ho0sub

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	ho0sub	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}T=S{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to S{-}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T$$
2		oveq1	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to S{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)$$
3	1 2	eqeq12d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(S{-}_{\mathrm{op}}T=S{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)\leftrightarrow if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)\right)$$
4		oveq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
5		oveq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to 0_{\mathrm{hop}}{-}_{\mathrm{op}}T=0_{\mathrm{hop}}{-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
6	5	oveq2d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
7	4 6	eqeq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)\leftrightarrow if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)\right)$$
8		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
9	8	elimf	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
10	8	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
11	9 10	ho0subi	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
12	3 7 11	dedth2h	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}T=S{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}T\right)$$