Metamath Proof Explorer

Theorem adjvalval

Description: Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Assertion adjvalval 
|- ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) = ( iota_ w e. ~H A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) ) )

Proof

Step Hyp Ref Expression
1 adjcl 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) e. ~H )
2 eqcom 
 |-  ( ( ( T ` x ) .ih A ) = ( x .ih w ) <-> ( x .ih w ) = ( ( T ` x ) .ih A ) )
3 adj2 
 |-  ( ( T e. dom adjh /\ x e. ~H /\ A e. ~H ) -> ( ( T ` x ) .ih A ) = ( x .ih ( ( adjh ` T ) ` A ) ) )
4 3 3com23 
 |-  ( ( T e. dom adjh /\ A e. ~H /\ x e. ~H ) -> ( ( T ` x ) .ih A ) = ( x .ih ( ( adjh ` T ) ` A ) ) )
5 4 3expa 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ x e. ~H ) -> ( ( T ` x ) .ih A ) = ( x .ih ( ( adjh ` T ) ` A ) ) )
6 5 eqeq2d 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ x e. ~H ) -> ( ( x .ih w ) = ( ( T ` x ) .ih A ) <-> ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) ) )
7 2 6 syl5bb 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ x e. ~H ) -> ( ( ( T ` x ) .ih A ) = ( x .ih w ) <-> ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) ) )
8 7 ralbidva 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) <-> A. x e. ~H ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) ) )
9 8 adantr 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ w e. ~H ) -> ( A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) <-> A. x e. ~H ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) ) )
10 simpr 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ w e. ~H ) -> w e. ~H )
11 1 adantr 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ w e. ~H ) -> ( ( adjh ` T ) ` A ) e. ~H )
12 hial2eq2 
 |-  ( ( w e. ~H /\ ( ( adjh ` T ) ` A ) e. ~H ) -> ( A. x e. ~H ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) <-> w = ( ( adjh ` T ) ` A ) ) )
13 10 11 12 syl2anc 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ w e. ~H ) -> ( A. x e. ~H ( x .ih w ) = ( x .ih ( ( adjh ` T ) ` A ) ) <-> w = ( ( adjh ` T ) ` A ) ) )
14 9 13 bitrd 
 |-  ( ( ( T e. dom adjh /\ A e. ~H ) /\ w e. ~H ) -> ( A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) <-> w = ( ( adjh ` T ) ` A ) ) )
15 1 14 riota5 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( iota_ w e. ~H A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) ) = ( ( adjh ` T ) ` A ) )
16 15 eqcomd 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) = ( iota_ w e. ~H A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) ) )