Metamath Proof Explorer

Theorem adjval2

Description: Value of the adjoint function. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjval2 
|- ( T e. dom adjh -> ( adjh ` T ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 adjval 
 |-  ( T e. dom adjh -> ( adjh ` T ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
2 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
3 elmapi 
 |-  ( u e. ( ~H ^m ~H ) -> u : ~H --> ~H )
4 adjsym 
 |-  ( ( T : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( T ` x ) .ih y ) ) )
5 eqcom 
 |-  ( ( x .ih ( u ` y ) ) = ( ( T ` x ) .ih y ) <-> ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) )
6 5 2ralbii 
 |-  ( A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( T ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) )
7 4 6 bitrdi 
 |-  ( ( T : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )
8 2 3 7 syl2an 
 |-  ( ( T e. dom adjh /\ u e. ( ~H ^m ~H ) ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )
9 8 riotabidva 
 |-  ( T e. dom adjh -> ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )
10 1 9 eqtrd 
 |-  ( T e. dom adjh -> ( adjh ` T ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )