Metamath Proof Explorer

Theorem ajval

Description: Value of the adjoint function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajval.1 
|- X = ( BaseSet ` U )
ajval.2 
|- Y = ( BaseSet ` W )
ajval.3 
|- P = ( .iOLD ` U )
ajval.4 
|- Q = ( .iOLD ` W )
ajval.5 
|- A = ( U adj W )
Assertion ajval 
|- ( ( U e. CPreHilOLD /\ W e. NrmCVec /\ T : X --> Y ) -> ( A ` T ) = ( iota s ( 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 ajval.1 
 |-  X = ( BaseSet ` U )
2 ajval.2 
 |-  Y = ( BaseSet ` W )
3 ajval.3 
 |-  P = ( .iOLD ` U )
4 ajval.4 
 |-  Q = ( .iOLD ` W )
5 ajval.5 
 |-  A = ( U adj W )
6 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
7 1 2 3 4 5 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 ) ) ) } )
8 6 7 sylan 
 |-  ( ( U e. CPreHilOLD /\ 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 ) ) ) } )
9 8 fveq1d 
 |-  ( ( U e. CPreHilOLD /\ W e. NrmCVec ) -> ( A ` T ) = ( { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } ` T ) )
10 9 3adant3 
 |-  ( ( U e. CPreHilOLD /\ W e. NrmCVec /\ T : X --> Y ) -> ( A ` T ) = ( { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } ` T ) )
11 1 fvexi 
 |-  X e. _V
12 fex 
 |-  ( ( T : X --> Y /\ X e. _V ) -> T e. _V )
13 11 12 mpan2 
 |-  ( T : X --> Y -> T e. _V )
14 eqid 
 |-  { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q 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 ) ) ) }
15 feq1 
 |-  ( t = T -> ( t : X --> Y <-> T : X --> Y ) )
16 fveq1 
 |-  ( t = T -> ( t ` x ) = ( T ` x ) )
17 16 oveq1d 
 |-  ( t = T -> ( ( t ` x ) Q y ) = ( ( T ` x ) Q y ) )
18 17 eqeq1d 
 |-  ( t = T -> ( ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) <-> ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) )
19 18 2ralbidv 
 |-  ( t = T -> ( A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) <-> A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) )
20 15 19 3anbi13d 
 |-  ( t = T -> ( ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q 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 ) ) ) ) )
21 14 20 fvopab5 
 |-  ( T e. _V -> ( { <. t , s >. | ( t : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( t ` x ) Q y ) = ( x P ( s ` y ) ) ) } ` T ) = ( iota s ( T : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
22 13 21 syl 
 |-  ( T : X --> 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 ) ) ) } ` T ) = ( iota s ( T : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
23 3anass 
 |-  ( ( T : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q 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 ) ) ) ) )
24 23 baib 
 |-  ( T : X --> Y -> ( ( T : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) <-> ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
25 24 iotabidv 
 |-  ( T : X --> Y -> ( iota s ( T : X --> Y /\ s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) = ( iota s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
26 22 25 eqtrd 
 |-  ( T : X --> 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 ) ) ) } ` T ) = ( iota s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
27 26 3ad2ant3 
 |-  ( ( U e. CPreHilOLD /\ W e. NrmCVec /\ T : X --> 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 ) ) ) } ` T ) = ( iota s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )
28 10 27 eqtrd 
 |-  ( ( U e. CPreHilOLD /\ W e. NrmCVec /\ T : X --> Y ) -> ( A ` T ) = ( iota s ( s : Y --> X /\ A. x e. X A. y e. Y ( ( T ` x ) Q y ) = ( x P ( s ` y ) ) ) ) )