This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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