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ℎ ‘ 𝑇 ) ) = 𝑇 )