Theorem lnfnli

Description: Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnfnl.1	|- T e. LinFn
Assertion	lnfnli	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )

Proof

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