Metamath Proof Explorer

Theorem adjval

Description: Value of the adjoint function for T in the domain of adjh . (Contributed by NM, 19-Feb-2006) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
2 1 biantrurd 
 |-  ( T e. dom adjh -> ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) )
3 ax-hilex 
 |-  ~H e. _V
4 3 3 elmap 
 |-  ( u e. ( ~H ^m ~H ) <-> u : ~H --> ~H )
5 4 anbi1i 
 |-  ( ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
6 3anass 
 |-  ( ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
7 2 5 6 3bitr4g 
 |-  ( 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 ) ) <-> ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
8 7 iotabidv 
 |-  ( T e. dom adjh -> ( iota u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) = ( iota u ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
9 df-riota 
 |-  ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) = ( iota u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
10 9 a1i 
 |-  ( 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 ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
11 dfadj2 
 |-  adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
12 feq1 
 |-  ( t = T -> ( t : ~H --> ~H <-> T : ~H --> ~H ) )
13 fveq1 
 |-  ( t = T -> ( t ` y ) = ( T ` y ) )
14 13 oveq2d 
 |-  ( t = T -> ( x .ih ( t ` y ) ) = ( x .ih ( T ` y ) ) )
15 14 eqeq1d 
 |-  ( t = T -> ( ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
16 15 2ralbidv 
 |-  ( t = T -> ( 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 ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
17 12 16 3anbi13d 
 |-  ( t = T -> ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
18 11 17 fvopab5 
 |-  ( T e. dom adjh -> ( adjh ` T ) = ( iota u ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) )
19 8 10 18 3eqtr4rd 
 |-  ( 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 ) ) )