Metamath Proof Explorer

Theorem ajfval

Description: The adjoint function. (Contributed by NM, 25-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ajfval.1 
|- X = ( BaseSet ` U )
ajfval.2 
|- Y = ( BaseSet ` W )
ajfval.3 
|- P = ( .iOLD ` U )
ajfval.4 
|- Q = ( .iOLD ` W )
ajfval.5 
|- A = ( U adj W )
Assertion ajfval 
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> A = { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 ajfval.1 
 |-  X = ( BaseSet ` U )
2 ajfval.2 
 |-  Y = ( BaseSet ` W )
3 ajfval.3 
 |-  P = ( .iOLD ` U )
4 ajfval.4 
 |-  Q = ( .iOLD ` W )
5 ajfval.5 
 |-  A = ( U adj W )
6 fveq2 
 |-  ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
7 6 1 eqtr4di 
 |-  ( u = U -> ( BaseSet ` u ) = X )
8 7 feq2d 
 |-  ( u = U -> ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) <-> t : X --> ( BaseSet ` w ) ) )
9 7 feq3d 
 |-  ( u = U -> ( s : ( BaseSet ` w ) --> ( BaseSet ` u ) <-> s : ( BaseSet ` w ) --> X ) )
10 fveq2 
 |-  ( u = U -> ( .iOLD ` u ) = ( .iOLD ` U ) )
11 10 3 eqtr4di 
 |-  ( u = U -> ( .iOLD ` u ) = P )
12 11 oveqd 
 |-  ( u = U -> ( x ( .iOLD ` u ) ( s ` y ) ) = ( x P ( s ` y ) ) )
13 12 eqeq2d 
 |-  ( u = U -> ( ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) <-> ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) )
14 13 ralbidv 
 |-  ( u = U -> ( A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) <-> A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) )
15 7 14 raleqbidv 
 |-  ( u = U -> ( A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) <-> A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) )
16 8 9 15 3anbi123d 
 |-  ( u = U -> ( ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) <-> ( t : X --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> X /\ A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) ) )
17 16 opabbidv 
 |-  ( u = U -> { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) } = { <. t , s >. | ( t : X --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> X /\ A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) } )
18 fveq2 
 |-  ( w = W -> ( BaseSet ` w ) = ( BaseSet ` W ) )
19 18 2 eqtr4di 
 |-  ( w = W -> ( BaseSet ` w ) = Y )
20 19 feq3d 
 |-  ( w = W -> ( t : X --> ( BaseSet ` w ) <-> t : X --> Y ) )
21 19 feq2d 
 |-  ( w = W -> ( s : ( BaseSet ` w ) --> X <-> s : Y --> X ) )
22 fveq2 
 |-  ( w = W -> ( .iOLD ` w ) = ( .iOLD ` W ) )
23 22 4 eqtr4di 
 |-  ( w = W -> ( .iOLD ` w ) = Q )
24 23 oveqd 
 |-  ( w = W -> ( ( t ` x ) ( .iOLD ` w ) y ) = ( ( t ` x ) Q y ) )
25 24 eqeq1d 
 |-  ( w = W -> ( ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) <-> ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) )
26 19 25 raleqbidv 
 |-  ( w = W -> ( A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) <-> A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) )
27 26 ralbidv 
 |-  ( w = W -> ( A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) <-> A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) )
28 20 21 27 3anbi123d 
 |-  ( w = W -> ( ( t : X --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> X /\ A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) <-> ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
29 28 opabbidv 
 |-  ( w = W -> { <. t , s >. | ( t : X --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> X /\ A. x e. X A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x P ( s ` y ) ) ) } = { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } )
30 df-aj 
 |-  adj = ( u e. NrmCVec , w e. NrmCVec |-> { <. t , s >. | ( t : ( BaseSet ` u ) --> ( BaseSet ` w ) /\ s : ( BaseSet ` w ) --> ( BaseSet ` u ) /\ A. x e. ( BaseSet ` u ) A. y e. ( BaseSet ` w ) ( ( t ` x ) ( .iOLD ` w ) y ) = ( x ( .iOLD ` u ) ( s ` y ) ) ) } )
31 ovex 
 |-  ( Y ^m X ) e. _V
32 ovex 
 |-  ( X ^m Y ) e. _V
33 31 32 xpex 
 |-  ( ( Y ^m X ) X. ( X ^m Y ) ) e. _V
34 2 fvexi 
 |-  Y e. _V
35 1 fvexi 
 |-  X e. _V
36 34 35 elmap 
 |-  ( t e. ( Y ^m X ) <-> t : X --> Y )
37 35 34 elmap 
 |-  ( s e. ( X ^m Y ) <-> s : Y --> X )
38 36 37 anbi12i 
 |-  ( ( t e. ( Y ^m X ) /\ s e. ( X ^m Y ) ) <-> ( t : X --> Y /\ s : Y --> X ) )
39 38 biimpri 
 |-  ( ( t : X --> Y /\ s : Y --> X ) -> ( t e. ( Y ^m X ) /\ s e. ( X ^m Y ) ) )
40 39 3adant3 
 |-  ( ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) -> ( t e. ( Y ^m X ) /\ s e. ( X ^m Y ) ) )
41 40 ssopab2i 
 |-  { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } C_ { <. t , s >. | ( t e. ( Y ^m X ) /\ s e. ( X ^m Y ) ) }
42 df-xp 
 |-  ( ( Y ^m X ) X. ( X ^m Y ) ) = { <. t , s >. | ( t e. ( Y ^m X ) /\ s e. ( X ^m Y ) ) }
43 41 42 sseqtrri 
 |-  { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } C_ ( ( Y ^m X ) X. ( X ^m Y ) )
44 33 43 ssexi 
 |-  { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } e. _V
45 17 29 30 44 ovmpo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U adj W ) = { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } )
46 5 45 eqtrid 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> A = { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } )