Theorem lnopmuli

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopl.1	|- T e. LinOp
Assertion	lnopmuli	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	|- T e. LinOp
2		lnopmul	|- ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )
3	1 2	mp3an1	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )