Metamath Proof Explorer

Theorem adjadj

Description: Double adjoint. Theorem 3.11(iv) of Beran p. 106. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adjadj	⊢ ( 𝑇 ∈ dom adj_ℎ → ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		adj2	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
2		dmadjrn	⊢ ( 𝑇 ∈ dom adj_ℎ → ( adj_ℎ ‘ 𝑇 ) ∈ dom adj_ℎ )
3		adj1	⊢ ( ( ( adj_ℎ ‘ 𝑇 ) ∈ dom adj_ℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝑦 ) ) = ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) )
4	2 3	syl3an1	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝑦 ) ) = ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) )
5	1 4	eqtr2d	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) )
6	5	3expib	⊢ ( 𝑇 ∈ dom adj_ℎ → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
7	6	ralrimivv	⊢ ( 𝑇 ∈ dom adj_ℎ → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) )
8		dmadjrn	⊢ ( ( adj_ℎ ‘ 𝑇 ) ∈ dom adj_ℎ → ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ∈ dom adj_ℎ )
9		dmadjop	⊢ ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ∈ dom adj_ℎ → ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ )
10	2 8 9	3syl	⊢ ( 𝑇 ∈ dom adj_ℎ → ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ )
11		dmadjop	⊢ ( 𝑇 ∈ dom adj_ℎ → 𝑇 : ℋ ⟶ ℋ )
12		hoeq1	⊢ ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ↔ ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) = 𝑇 ) )
13	10 11 12	syl2anc	⊢ ( 𝑇 ∈ dom adj_ℎ → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) ↔ ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) = 𝑇 ) )
14	7 13	mpbid	⊢ ( 𝑇 ∈ dom adj_ℎ → ( adj_ℎ ‘ ( adj_ℎ ‘ 𝑇 ) ) = 𝑇 )