Theorem hosubcl

Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

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

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	1	feq1d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\leftrightarrow \left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\right)$$
3		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)$$
4	3	feq1d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\leftrightarrow \left(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)\right):\mathscr{H}⟶\mathscr{H}\right)$$
5		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
6	5	elimf	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
7	5	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
8	6 7	hosubcli	$$⊢\left(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)\right):\mathscr{H}⟶\mathscr{H}$$
9	2 4 8	dedth2h	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$