Metamath Proof Explorer

Theorem hfmval

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

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

Proof

Step Hyp Ref Expression
1 hfmmval 
 |-  ( ( A e. CC /\ T : ~H --> CC ) -> ( A .fn T ) = ( x e. ~H |-> ( A x. ( T ` x ) ) ) )
2 1 fveq1d 
 |-  ( ( A e. CC /\ T : ~H --> CC ) -> ( ( A .fn T ) ` B ) = ( ( x e. ~H |-> ( A x. ( T ` x ) ) ) ` B ) )
3 fveq2 
 |-  ( x = B -> ( T ` x ) = ( T ` B ) )
4 3 oveq2d 
 |-  ( x = B -> ( A x. ( T ` x ) ) = ( A x. ( T ` B ) ) )
5 eqid 
 |-  ( x e. ~H |-> ( A x. ( T ` x ) ) ) = ( x e. ~H |-> ( A x. ( T ` x ) ) )
6 ovex 
 |-  ( A x. ( T ` B ) ) e. _V
7 4 5 6 fvmpt 
 |-  ( B e. ~H -> ( ( x e. ~H |-> ( A x. ( T ` x ) ) ) ` B ) = ( A x. ( T ` B ) ) )
8 2 7 sylan9eq 
 |-  ( ( ( A e. CC /\ T : ~H --> CC ) /\ B e. ~H ) -> ( ( A .fn T ) ` B ) = ( A x. ( T ` B ) ) )
9 8 3impa 
 |-  ( ( A e. CC /\ T : ~H --> CC /\ B e. ~H ) -> ( ( A .fn T ) ` B ) = ( A x. ( T ` B ) ) )