Theorem hodcli

Description: Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3		hodcl	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)\in \mathscr{H}$$
4	1 2 3	mpanl12	$$⊢A\in \mathscr{H}\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)\in \mathscr{H}$$