Metamath Proof Explorer

Theorem cnvadj

Description: The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvadj 
|- `' adjh = adjh

Proof

Step Hyp Ref Expression
1 cnvopab 
 |-  `' { <. u , t >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) } = { <. t , u >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) }
2 3ancoma 
 |-  ( ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) <-> ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) )
3 ffvelrn 
 |-  ( ( u : ~H --> ~H /\ y e. ~H ) -> ( u ` y ) e. ~H )
4 ax-his1 
 |-  ( ( ( u ` y ) e. ~H /\ x e. ~H ) -> ( ( u ` y ) .ih x ) = ( * ` ( x .ih ( u ` y ) ) ) )
5 3 4 sylan 
 |-  ( ( ( u : ~H --> ~H /\ y e. ~H ) /\ x e. ~H ) -> ( ( u ` y ) .ih x ) = ( * ` ( x .ih ( u ` y ) ) ) )
6 5 adantrl 
 |-  ( ( ( u : ~H --> ~H /\ y e. ~H ) /\ ( t : ~H --> ~H /\ x e. ~H ) ) -> ( ( u ` y ) .ih x ) = ( * ` ( x .ih ( u ` y ) ) ) )
7 ffvelrn 
 |-  ( ( t : ~H --> ~H /\ x e. ~H ) -> ( t ` x ) e. ~H )
8 ax-his1 
 |-  ( ( y e. ~H /\ ( t ` x ) e. ~H ) -> ( y .ih ( t ` x ) ) = ( * ` ( ( t ` x ) .ih y ) ) )
9 7 8 sylan2 
 |-  ( ( y e. ~H /\ ( t : ~H --> ~H /\ x e. ~H ) ) -> ( y .ih ( t ` x ) ) = ( * ` ( ( t ` x ) .ih y ) ) )
10 9 adantll 
 |-  ( ( ( u : ~H --> ~H /\ y e. ~H ) /\ ( t : ~H --> ~H /\ x e. ~H ) ) -> ( y .ih ( t ` x ) ) = ( * ` ( ( t ` x ) .ih y ) ) )
11 6 10 eqeq12d 
 |-  ( ( ( u : ~H --> ~H /\ y e. ~H ) /\ ( t : ~H --> ~H /\ x e. ~H ) ) -> ( ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) <-> ( * ` ( x .ih ( u ` y ) ) ) = ( * ` ( ( t ` x ) .ih y ) ) ) )
12 11 ancoms 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) <-> ( * ` ( x .ih ( u ` y ) ) ) = ( * ` ( ( t ` x ) .ih y ) ) ) )
13 hicl 
 |-  ( ( x e. ~H /\ ( u ` y ) e. ~H ) -> ( x .ih ( u ` y ) ) e. CC )
14 3 13 sylan2 
 |-  ( ( x e. ~H /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( x .ih ( u ` y ) ) e. CC )
15 14 adantll 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( x .ih ( u ` y ) ) e. CC )
16 hicl 
 |-  ( ( ( t ` x ) e. ~H /\ y e. ~H ) -> ( ( t ` x ) .ih y ) e. CC )
17 7 16 sylan 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ y e. ~H ) -> ( ( t ` x ) .ih y ) e. CC )
18 17 adantrl 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( ( t ` x ) .ih y ) e. CC )
19 cj11 
 |-  ( ( ( x .ih ( u ` y ) ) e. CC /\ ( ( t ` x ) .ih y ) e. CC ) -> ( ( * ` ( x .ih ( u ` y ) ) ) = ( * ` ( ( t ` x ) .ih y ) ) <-> ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) )
20 15 18 19 syl2anc 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( ( * ` ( x .ih ( u ` y ) ) ) = ( * ` ( ( t ` x ) .ih y ) ) <-> ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) )
21 12 20 bitr2d 
 |-  ( ( ( t : ~H --> ~H /\ x e. ~H ) /\ ( u : ~H --> ~H /\ y e. ~H ) ) -> ( ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) ) )
22 21 an4s 
 |-  ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) ) )
23 22 anassrs 
 |-  ( ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ x e. ~H ) /\ y e. ~H ) -> ( ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) ) )
24 eqcom 
 |-  ( ( ( u ` y ) .ih x ) = ( y .ih ( t ` x ) ) <-> ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) )
25 23 24 bitrdi 
 |-  ( ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ x e. ~H ) /\ y e. ~H ) -> ( ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
26 25 ralbidva 
 |-  ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ x e. ~H ) -> ( A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> A. y e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
27 26 ralbidva 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
28 ralcom 
 |-  ( A. x e. ~H A. y e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) <-> A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) )
29 27 28 bitrdi 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) <-> A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
30 29 pm5.32i 
 |-  ( ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
31 df-3an 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) )
32 df-3an 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) <-> ( ( t : ~H --> ~H /\ u : ~H --> ~H ) /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
33 30 31 32 3bitr4i 
 |-  ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) <-> ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
34 2 33 bitri 
 |-  ( ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) <-> ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) )
35 34 opabbii 
 |-  { <. t , u >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) } = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) }
36 1 35 eqtri 
 |-  `' { <. u , t >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) } = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) }
37 dfadj2 
 |-  adjh = { <. u , t >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) }
38 37 cnveqi 
 |-  `' adjh = `' { <. u , t >. | ( u : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( u ` y ) ) = ( ( t ` x ) .ih y ) ) }
39 dfadj2 
 |-  adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. y e. ~H A. x e. ~H ( y .ih ( t ` x ) ) = ( ( u ` y ) .ih x ) ) }
40 36 38 39 3eqtr4i 
 |-  `' adjh = adjh