Theorem ho2coi

Description: Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	ho2coi	$$⊢A\in \mathscr{H}\to \left(\left(R\circ S\right)\circ T\right)\left(A\right)=R\left(S\left(T\left(A\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
2		hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	1 2	hocofi	$$⊢\left(R\circ S\right):\mathscr{H}⟶\mathscr{H}$$
5	4 3	hocoi	$$⊢A\in \mathscr{H}\to \left(\left(R\circ S\right)\circ T\right)\left(A\right)=\left(R\circ S\right)\left(T\left(A\right)\right)$$
6	3	ffvelrni	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
7	1 2	hocoi	$$⊢T\left(A\right)\in \mathscr{H}\to \left(R\circ S\right)\left(T\left(A\right)\right)=R\left(S\left(T\left(A\right)\right)\right)$$
8	6 7	syl	$$⊢A\in \mathscr{H}\to \left(R\circ S\right)\left(T\left(A\right)\right)=R\left(S\left(T\left(A\right)\right)\right)$$
9	5 8	eqtrd	$$⊢A\in \mathscr{H}\to \left(\left(R\circ S\right)\circ T\right)\left(A\right)=R\left(S\left(T\left(A\right)\right)\right)$$