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 adj h -1 = adj h

Proof

Step Hyp Ref Expression
1 cnvopab u t | u : t : x y x ih u y = t x ih y -1 = t u | u : t : x y x ih u y = t x ih y
2 3ancoma u : t : x y x ih u y = t x ih y t : u : x y x ih u y = t x ih y
3 ffvelrn u : y u y
4 ax-his1 u y x u y ih x = x ih u y
5 3 4 sylan u : y x u y ih x = x ih u y
6 5 adantrl u : y t : x u y ih x = x ih u y
7 ffvelrn t : x t x
8 ax-his1 y t x y ih t x = t x ih y
9 7 8 sylan2 y t : x y ih t x = t x ih y
10 9 adantll u : y t : x y ih t x = t x ih y
11 6 10 eqeq12d u : y t : x u y ih x = y ih t x x ih u y = t x ih y
12 11 ancoms t : x u : y u y ih x = y ih t x x ih u y = t x ih y
13 hicl x u y x ih u y
14 3 13 sylan2 x u : y x ih u y
15 14 adantll t : x u : y x ih u y
16 hicl t x y t x ih y
17 7 16 sylan t : x y t x ih y
18 17 adantrl t : x u : y t x ih y
19 cj11 x ih u y t x ih y x ih u y = t x ih y x ih u y = t x ih y
20 15 18 19 syl2anc t : x u : y x ih u y = t x ih y x ih u y = t x ih y
21 12 20 bitr2d t : x u : y x ih u y = t x ih y u y ih x = y ih t x
22 21 an4s t : u : x y x ih u y = t x ih y u y ih x = y ih t x
23 22 anassrs t : u : x y 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 : u : x y x ih u y = t x ih y y ih t x = u y ih x
26 25 ralbidva t : u : x y x ih u y = t x ih y y y ih t x = u y ih x
27 26 ralbidva t : u : x y x ih u y = t x ih y x y y ih t x = u y ih x
28 ralcom x y y ih t x = u y ih x y x y ih t x = u y ih x
29 27 28 bitrdi t : u : x y x ih u y = t x ih y y x y ih t x = u y ih x
30 29 pm5.32i t : u : x y x ih u y = t x ih y t : u : y x y ih t x = u y ih x
31 df-3an t : u : x y x ih u y = t x ih y t : u : x y x ih u y = t x ih y
32 df-3an t : u : y x y ih t x = u y ih x t : u : y x y ih t x = u y ih x
33 30 31 32 3bitr4i t : u : x y x ih u y = t x ih y t : u : y x y ih t x = u y ih x
34 2 33 bitri u : t : x y x ih u y = t x ih y t : u : y x y ih t x = u y ih x
35 34 opabbii t u | u : t : x y x ih u y = t x ih y = t u | t : u : y x y ih t x = u y ih x
36 1 35 eqtri u t | u : t : x y x ih u y = t x ih y -1 = t u | t : u : y x y ih t x = u y ih x
37 dfadj2 adj h = u t | u : t : x y x ih u y = t x ih y
38 37 cnveqi adj h -1 = u t | u : t : x y x ih u y = t x ih y -1
39 dfadj2 adj h = t u | t : u : y x y ih t x = u y ih x
40 36 38 39 3eqtr4i adj h -1 = adj h