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 : ~H --> ~H
	hods.2	|- S : ~H --> ~H
	hods.3	|- T : ~H --> ~H
Assertion	ho2coi	|- ( A e. ~H -> ( ( ( R o. S ) o. T ) ` A ) = ( R ` ( S ` ( T ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hods.1	|- R : ~H --> ~H
2		hods.2	|- S : ~H --> ~H
3		hods.3	|- T : ~H --> ~H
4	1 2	hocofi	|- ( R o. S ) : ~H --> ~H
5	4 3	hocoi	|- ( A e. ~H -> ( ( ( R o. S ) o. T ) ` A ) = ( ( R o. S ) ` ( T ` A ) ) )
6	3	ffvelrni	|- ( A e. ~H -> ( T ` A ) e. ~H )
7	1 2	hocoi	|- ( ( T ` A ) e. ~H -> ( ( R o. S ) ` ( T ` A ) ) = ( R ` ( S ` ( T ` A ) ) ) )
8	6 7	syl	|- ( A e. ~H -> ( ( R o. S ) ` ( T ` A ) ) = ( R ` ( S ` ( T ` A ) ) ) )
9	5 8	eqtrd	|- ( A e. ~H -> ( ( ( R o. S ) o. T ) ` A ) = ( R ` ( S ` ( T ` A ) ) ) )