Theorem hococli

Description: Closure of composition of Hilbert space operators. (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	hococli	$$⊢A\in \mathscr{H}\to \left(S\circ 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	1 2	hocoi	$$⊢A\in \mathscr{H}\to \left(S\circ T\right)\left(A\right)=S\left(T\left(A\right)\right)$$
4	2	ffvelrni	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
5	1	ffvelrni	$$⊢T\left(A\right)\in \mathscr{H}\to S\left(T\left(A\right)\right)\in \mathscr{H}$$
6	4 5	syl	$$⊢A\in \mathscr{H}\to S\left(T\left(A\right)\right)\in \mathscr{H}$$
7	3 6	eqeltrd	$$⊢A\in \mathscr{H}\to \left(S\circ T\right)\left(A\right)\in \mathscr{H}$$