Theorem hosubfni

Description: Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hosubfni	$$⊢\left(S{-}_{\mathrm{op}}T\right)Fn\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3	1 2	hosubcli	$$⊢\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
4		ffn	$$⊢\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\to \left(S{-}_{\mathrm{op}}T\right)Fn\mathscr{H}$$
5	3 4	ax-mp	$$⊢\left(S{-}_{\mathrm{op}}T\right)Fn\mathscr{H}$$