Theorem lnfnmuli

Description: Multiplicative 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	lnfnmuli	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnfnl.1	|- T e. LinFn
2		ax-hv0cl	|- 0h e. ~H
3	1	lnfnli	|- ( ( A e. CC /\ B e. ~H /\ 0h e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( ( A x. ( T ` B ) ) + ( T ` 0h ) ) )
4	2 3	mp3an3	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( ( A x. ( T ` B ) ) + ( T ` 0h ) ) )
5		hvmulcl	|- ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
6		ax-hvaddid	|- ( ( A .h B ) e. ~H -> ( ( A .h B ) +h 0h ) = ( A .h B ) )
7	5 6	syl	|- ( ( A e. CC /\ B e. ~H ) -> ( ( A .h B ) +h 0h ) = ( A .h B ) )
8	7	fveq2d	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( T ` ( A .h B ) ) )
9	1	lnfn0i	|- ( T ` 0h ) = 0
10	9	oveq2i	|- ( ( A x. ( T ` B ) ) + ( T ` 0h ) ) = ( ( A x. ( T ` B ) ) + 0 )
11	1	lnfnfi	|- T : ~H --> CC
12	11	ffvelcdmi	|- ( B e. ~H -> ( T ` B ) e. CC )
13		mulcl	|- ( ( A e. CC /\ ( T ` B ) e. CC ) -> ( A x. ( T ` B ) ) e. CC )
14	12 13	sylan2	|- ( ( A e. CC /\ B e. ~H ) -> ( A x. ( T ` B ) ) e. CC )
15	14	addridd	|- ( ( A e. CC /\ B e. ~H ) -> ( ( A x. ( T ` B ) ) + 0 ) = ( A x. ( T ` B ) ) )
16	10 15	eqtrid	|- ( ( A e. CC /\ B e. ~H ) -> ( ( A x. ( T ` B ) ) + ( T ` 0h ) ) = ( A x. ( T ` B ) ) )
17	4 8 16	3eqtr3d	|- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) )