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