Metamath Proof Explorer

Theorem homval

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

Ref Expression
Assertion homval 
|- ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) = ( A .h ( T ` B ) ) )

Proof

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