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

Proof

Step Hyp Ref Expression
1 cnvopab { ⟨ 𝑢 , 𝑡 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) }
2 3ancoma ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
3 ffvelrn ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑢𝑦 ) ∈ ℋ )
4 ax-his1 ( ( ( 𝑢𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) )
5 3 4 sylan ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) )
6 5 adantrl ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) )
7 ffvelrn ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑡𝑥 ) ∈ ℋ )
8 ax-his1 ( ( 𝑦 ∈ ℋ ∧ ( 𝑡𝑥 ) ∈ ℋ ) → ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
9 7 8 sylan2 ( ( 𝑦 ∈ ℋ ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
10 9 adantll ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
11 6 10 eqeq12d ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ) )
12 11 ancoms ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ) )
13 hicl ( ( 𝑥 ∈ ℋ ∧ ( 𝑢𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑢𝑦 ) ) ∈ ℂ )
14 3 13 sylan2 ( ( 𝑥 ∈ ℋ ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑢𝑦 ) ) ∈ ℂ )
15 14 adantll ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑢𝑦 ) ) ∈ ℂ )
16 hicl ( ( ( 𝑡𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∈ ℂ )
17 7 16 sylan ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∈ ℂ )
18 17 adantrl ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∈ ℂ )
19 cj11 ( ( ( 𝑥 ·ih ( 𝑢𝑦 ) ) ∈ ℂ ∧ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∈ ℂ ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
20 15 18 19 syl2anc ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑢𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
21 12 20 bitr2d ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ) )
22 21 an4s ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ) )
23 22 anassrs ( ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ) )
24 eqcom ( ( ( 𝑢𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑡𝑥 ) ) ↔ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) )
25 23 24 bitrdi ( ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
26 25 ralbidva ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
27 26 ralbidva ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
28 ralcom ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) )
29 27 28 bitrdi ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
30 29 pm5.32i ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
31 df-3an ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
32 df-3an ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) ↔ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
33 30 31 32 3bitr4i ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
34 2 33 bitri ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) )
35 34 opabbii { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) }
36 1 35 eqtri { ⟨ 𝑢 , 𝑡 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) }
37 dfadj2 adj = { ⟨ 𝑢 , 𝑡 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) }
38 37 cnveqi adj = { ⟨ 𝑢 , 𝑡 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) }
39 dfadj2 adj = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 ·ih ( 𝑡𝑥 ) ) = ( ( 𝑢𝑦 ) ·ih 𝑥 ) ) }
40 36 38 39 3eqtr4i adj = adj