Theorem hocoi

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

	Ref	Expression
Hypotheses	hoeq.1	|- S : ~H --> ~H
	hoeq.2	|- T : ~H --> ~H
Assertion	hocoi	|- ( A e. ~H -> ( ( S o. T ) ` A ) = ( S ` ( T ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	|- S : ~H --> ~H
2		hoeq.2	|- T : ~H --> ~H
3		fvco3	|- ( ( T : ~H --> ~H /\ A e. ~H ) -> ( ( S o. T ) ` A ) = ( S ` ( T ` A ) ) )
4	2 3	mpan	|- ( A e. ~H -> ( ( S o. T ) ` A ) = ( S ` ( T ` A ) ) )