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		ffvelcdm	⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑢 ‘ 𝑦 ) ∈ ℋ )
4		ax-his1	⊢ ( ( ( 𝑢 ‘ 𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢 ‘ 𝑦 ) ·_ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·_ih ( 𝑢 ‘ 𝑦 ) ) ) )
5	3 4	sylan	⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑢 ‘ 𝑦 ) ·_ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·_ih ( 𝑢 ‘ 𝑦 ) ) ) )
6	5	adantrl	⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑢 ‘ 𝑦 ) ·_ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·_ih ( 𝑢 ‘ 𝑦 ) ) ) )
7		ffvelcdm	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑡 ‘ 𝑥 ) ∈ ℋ )
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_ℎ

Metamath Proof Explorer

Theorem cnvadj

Proof