Theorem hoscl

Description: Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	hoscl	$$⊢\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		hosval	$$⊢\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	1	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)=S\left(A\right){+}_{ℎ}T\left(A\right)$$
3		ffvelrn	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to S\left(A\right)\in \mathscr{H}$$
4		ffvelrn	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to T\left(A\right)\in \mathscr{H}$$
5	3 4	anim12i	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\right)\to \left(S\left(A\right)\in \mathscr{H}\wedge T\left(A\right)\in \mathscr{H}\right)$$
6	5	anandirs	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge A\in \mathscr{H}\right)\to \left(S\left(A\right)\in \mathscr{H}\wedge T\left(A\right)\in \mathscr{H}\right)$$
7		hvaddcl	$$⊢\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}$$
8	6 7	syl	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge A\in \mathscr{H}\right)\to S\left(A\right){+}_{ℎ}T\left(A\right)\in \mathscr{H}$$
9	2 8	eqeltrd	$$⊢\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}$$