Metamath Proof Explorer

Theorem hmopadj

Description: A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopadj 
|- ( T e. HrmOp -> ( adjh ` T ) = T )

Proof

Step Hyp Ref Expression
1 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
2 hmop 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
3 2 eqcomd 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( T ` y ) ) )
4 3 3expib 
 |-  ( T e. HrmOp -> ( ( x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( T ` y ) ) ) )
5 4 ralrimivv 
 |-  ( T e. HrmOp -> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( T ` y ) ) )
6 adjeq 
 |-  ( ( T : ~H --> ~H /\ T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( T ` y ) ) ) -> ( adjh ` T ) = T )
7 1 1 5 6 syl3anc 
 |-  ( T e. HrmOp -> ( adjh ` T ) = T )