Theorem hfmmval

Description: Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hfmmval	|- ( ( A e. CC /\ T : ~H --> CC ) -> ( A .fn T ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnex	|- CC e. _V
2		ax-hilex	|- ~H e. _V
3	1 2	elmap	|- ( T e. ( CC ^m ~H ) <-> T : ~H --> CC )
4		oveq1	|- ( f = A -> ( f x. ( g ` x ) ) = ( A x. ( g ` x ) ) )
5	4	mpteq2dv	|- ( f = A -> ( x e. ~H |-> ( f x. ( g ` x ) ) ) = ( x e. ~H |-> ( A x. ( g ` x ) ) ) )
6		fveq1	|- ( g = T -> ( g ` x ) = ( T ` x ) )
7	6	oveq2d	|- ( g = T -> ( A x. ( g ` x ) ) = ( A x. ( T ` x ) ) )
8	7	mpteq2dv	|- ( g = T -> ( x e. ~H |-> ( A x. ( g ` x ) ) ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )
9		df-hfmul	|- .fn = ( f e. CC , g e. ( CC ^m ~H ) |-> ( x e. ~H |-> ( f x. ( g ` x ) ) ) )
10	2	mptex	|- ( x e. ~H |-> ( A x. ( T ` x ) ) ) e. _V
11	5 8 9 10	ovmpo	|- ( ( A e. CC /\ T e. ( CC ^m ~H ) ) -> ( A .fn T ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )
12	3 11	sylan2br	|- ( ( A e. CC /\ T : ~H --> CC ) -> ( A .fn T ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )