Metamath Proof Explorer

Theorem hmopadj2

Description: An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in Halmos p. 41. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopadj2 
|- ( T e. dom adjh -> ( T e. HrmOp <-> ( adjh ` T ) = T ) )

Proof

Step Hyp Ref Expression
1 hmopadj 
 |-  ( T e. HrmOp -> ( adjh ` T ) = T )
2 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
3 2 adantr 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) = T ) -> T : ~H --> ~H )
4 adj1 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) )
5 4 3expb 
 |-  ( ( T e. dom adjh /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) )
6 5 adantlr 
 |-  ( ( ( T e. dom adjh /\ ( adjh ` T ) = T ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) = ( ( ( adjh ` T ) ` x ) .ih y ) )
7 fveq1 
 |-  ( ( adjh ` T ) = T -> ( ( adjh ` T ) ` x ) = ( T ` x ) )
8 7 oveq1d 
 |-  ( ( adjh ` T ) = T -> ( ( ( adjh ` T ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
9 8 ad2antlr 
 |-  ( ( ( T e. dom adjh /\ ( adjh ` T ) = T ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( adjh ` T ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
10 6 9 eqtrd 
 |-  ( ( ( T e. dom adjh /\ ( adjh ` T ) = T ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
11 10 ralrimivva 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) = T ) -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
12 elhmop 
 |-  ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
13 3 11 12 sylanbrc 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) = T ) -> T e. HrmOp )
14 13 ex 
 |-  ( T e. dom adjh -> ( ( adjh ` T ) = T -> T e. HrmOp ) )
15 1 14 impbid2 
 |-  ( T e. dom adjh -> ( T e. HrmOp <-> ( adjh ` T ) = T ) )