Metamath Proof Explorer

Theorem adjadj

Description: Double adjoint. Theorem 3.11(iv) of Beran p. 106. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjadj 
|- ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )

Proof

Step Hyp Ref Expression
1 adj2 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )
2 dmadjrn 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
3 adj1 
 |-  ( ( ( adjh ` T ) e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( ( adjh ` T ) ` y ) ) = ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) )
4 2 3 syl3an1 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( ( adjh ` T ) ` y ) ) = ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) )
5 1 4 eqtr2d 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
6 5 3expib 
 |-  ( T e. dom adjh -> ( ( x e. ~H /\ y e. ~H ) -> ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) ) )
7 6 ralrimivv 
 |-  ( T e. dom adjh -> A. x e. ~H A. y e. ~H ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
8 dmadjrn 
 |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` ( adjh ` T ) ) e. dom adjh )
9 dmadjop 
 |-  ( ( adjh ` ( adjh ` T ) ) e. dom adjh -> ( adjh ` ( adjh ` T ) ) : ~H --> ~H )
10 2 8 9 3syl 
 |-  ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) : ~H --> ~H )
11 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
12 hoeq1 
 |-  ( ( ( adjh ` ( adjh ` T ) ) : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) <-> ( adjh ` ( adjh ` T ) ) = T ) )
13 10 11 12 syl2anc 
 |-  ( T e. dom adjh -> ( A. x e. ~H A. y e. ~H ( ( ( adjh ` ( adjh ` T ) ) ` x ) .ih y ) = ( ( T ` x ) .ih y ) <-> ( adjh ` ( adjh ` T ) ) = T ) )
14 7 13 mpbid 
 |-  ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )