Metamath Proof Explorer

Theorem hmop

Description: Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmop 
|- ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )

Proof

Step Hyp Ref Expression
1 elhmop 
 |-  ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
2 1 simprbi 
 |-  ( T e. HrmOp -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
3 2 3ad2ant1 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
4 oveq1 
 |-  ( x = A -> ( x .ih ( T ` y ) ) = ( A .ih ( T ` y ) ) )
5 fveq2 
 |-  ( x = A -> ( T ` x ) = ( T ` A ) )
6 5 oveq1d 
 |-  ( x = A -> ( ( T ` x ) .ih y ) = ( ( T ` A ) .ih y ) )
7 4 6 eqeq12d 
 |-  ( x = A -> ( ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) <-> ( A .ih ( T ` y ) ) = ( ( T ` A ) .ih y ) ) )
8 fveq2 
 |-  ( y = B -> ( T ` y ) = ( T ` B ) )
9 8 oveq2d 
 |-  ( y = B -> ( A .ih ( T ` y ) ) = ( A .ih ( T ` B ) ) )
10 oveq2 
 |-  ( y = B -> ( ( T ` A ) .ih y ) = ( ( T ` A ) .ih B ) )
11 9 10 eqeq12d 
 |-  ( y = B -> ( ( A .ih ( T ` y ) ) = ( ( T ` A ) .ih y ) <-> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) ) )
12 7 11 rspc2v 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) ) )
13 12 3adant1 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) ) )
14 3 13 mpd 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )