Theorem hodcl

Description: Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	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}$$

Proof

Step	Hyp	Ref	Expression
1		hodval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$
2		ffvelcdm	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to S\left(A\right)\in \mathscr{H}$$
3	2	3adant2	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to S\left(A\right)\in \mathscr{H}$$
4		ffvelcdm	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to T\left(A\right)\in \mathscr{H}$$
5	4	3adant1	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to T\left(A\right)\in \mathscr{H}$$
6		hvsubcl	$$⊢\left(S\left(A\right)\in \mathscr{H}\wedge T\left(A\right)\in \mathscr{H}\right)\to S\left(A\right){-}_{ℎ}T\left(A\right)\in \mathscr{H}$$
7	3 5 6	syl2anc	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to S\left(A\right){-}_{ℎ}T\left(A\right)\in \mathscr{H}$$
8	1 7	eqeltrd	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)\in \mathscr{H}$$
9	8	3expa	$$⊢\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}$$