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-1=adjh

Proof

Step Hyp Ref Expression
1 cnvopab ⊢ut|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy-1=tu|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy
2 3ancoma ⊢u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy
3 ffvelcdm ⊢u:ℋ⟶ℋ∧y∈ℋ→u⁡y∈ℋ
4 ax-his1 ⊢u⁡y∈ℋ∧x∈ℋ→u⁡y⋅ihx=x⋅ihu⁡y‾
5 3 4 sylan ⊢u:ℋ⟶ℋ∧y∈ℋ∧x∈ℋ→u⁡y⋅ihx=x⋅ihu⁡y‾
6 5 adantrl ⊢u:ℋ⟶ℋ∧y∈ℋ∧t:ℋ⟶ℋ∧x∈ℋ→u⁡y⋅ihx=x⋅ihu⁡y‾
7 ffvelcdm ⊢t:ℋ⟶ℋ∧x∈ℋ→t⁡x∈ℋ
8 ax-his1 ⊢y∈ℋ∧t⁡x∈ℋ→y⋅iht⁡x=t⁡x⋅ihy‾
9 7 8 sylan2 ⊢y∈ℋ∧t:ℋ⟶ℋ∧x∈ℋ→y⋅iht⁡x=t⁡x⋅ihy‾
10 9 adantll ⊢u:ℋ⟶ℋ∧y∈ℋ∧t:ℋ⟶ℋ∧x∈ℋ→y⋅iht⁡x=t⁡x⋅ihy‾
11 6 10 eqeq12d ⊢u:ℋ⟶ℋ∧y∈ℋ∧t:ℋ⟶ℋ∧x∈ℋ→u⁡y⋅ihx=y⋅iht⁡x↔x⋅ihu⁡y‾=t⁡x⋅ihy‾
12 11 ancoms ⊢t:ℋ⟶ℋ∧x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→u⁡y⋅ihx=y⋅iht⁡x↔x⋅ihu⁡y‾=t⁡x⋅ihy‾
13 hicl ⊢x∈ℋ∧u⁡y∈ℋ→x⋅ihu⁡y∈ℂ
14 3 13 sylan2 ⊢x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→x⋅ihu⁡y∈ℂ
15 14 adantll ⊢t:ℋ⟶ℋ∧x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→x⋅ihu⁡y∈ℂ
16 hicl ⊢t⁡x∈ℋ∧y∈ℋ→t⁡x⋅ihy∈ℂ
17 7 16 sylan ⊢t:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→t⁡x⋅ihy∈ℂ
18 17 adantrl ⊢t:ℋ⟶ℋ∧x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→t⁡x⋅ihy∈ℂ
19 cj11 ⊢x⋅ihu⁡y∈ℂ∧t⁡x⋅ihy∈ℂ→x⋅ihu⁡y‾=t⁡x⋅ihy‾↔x⋅ihu⁡y=t⁡x⋅ihy
20 15 18 19 syl2anc ⊢t:ℋ⟶ℋ∧x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→x⋅ihu⁡y‾=t⁡x⋅ihy‾↔x⋅ihu⁡y=t⁡x⋅ihy
21 12 20 bitr2d ⊢t:ℋ⟶ℋ∧x∈ℋ∧u:ℋ⟶ℋ∧y∈ℋ→x⋅ihu⁡y=t⁡x⋅ihy↔u⁡y⋅ihx=y⋅iht⁡x
22 21 an4s ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihu⁡y=t⁡x⋅ihy↔u⁡y⋅ihx=y⋅iht⁡x
23 22 anassrs ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihu⁡y=t⁡x⋅ihy↔u⁡y⋅ihx=y⋅iht⁡x
24 eqcom ⊢u⁡y⋅ihx=y⋅iht⁡x↔y⋅iht⁡x=u⁡y⋅ihx
25 23 24 bitrdi ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihu⁡y=t⁡x⋅ihy↔y⋅iht⁡x=u⁡y⋅ihx
26 25 ralbidva ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧x∈ℋ→∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔∀y∈ℋy⋅iht⁡x=u⁡y⋅ihx
27 26 ralbidva ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔∀x∈ℋ∀y∈ℋy⋅iht⁡x=u⁡y⋅ihx
28 ralcom ⊢∀x∈ℋ∀y∈ℋy⋅iht⁡x=u⁡y⋅ihx↔∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
29 27 28 bitrdi ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
30 29 pm5.32i ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
31 df-3an ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy
32 df-3an ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
33 30 31 32 3bitr4i ⊢t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
34 2 33 bitri ⊢u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy↔t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
35 34 opabbii ⊢tu|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy=tu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
36 1 35 eqtri ⊢ut|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy-1=tu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
37 dfadj2 ⊢adjh=ut|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy
38 37 cnveqi ⊢adjh-1=ut|u:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihu⁡y=t⁡x⋅ihy-1
39 dfadj2 ⊢adjh=tu|t:ℋ⟶ℋ∧u:ℋ⟶ℋ∧∀y∈ℋ∀x∈ℋy⋅iht⁡x=u⁡y⋅ihx
40 36 38 39 3eqtr4i ⊢adjh-1=adjh