Theorem lnopli

Description: Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	|- T e. LinOp
2		lnopl	|- ( ( ( T e. LinOp /\ A e. CC ) /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A .h ( T ` B ) ) +h ( T ` C ) ) )
3	1 2	mpanl1	|- ( ( A e. CC /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A .h ( T ` B ) ) +h ( T ` C ) ) )
4	3	3impb	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A .h ( T ` B ) ) +h ( T ` C ) ) )