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 ) ) )`