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 ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T = T

Proof

Step Hyp Ref Expression
1 adj2 ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih y = x ⋅ ih adj h ⁡ T ⁡ y
2 dmadjrn ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h
3 adj1 ⊢ adj h ⁡ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih adj h ⁡ T ⁡ y = adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y
4 2 3 syl3an1 ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih adj h ⁡ T ⁡ y = adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y
5 1 4 eqtr2d ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y
6 5 3expib ⊢ T ∈ dom ⁡ adj h → x ∈ ℋ ∧ y ∈ ℋ → adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y
7 6 ralrimivv ⊢ T ∈ dom ⁡ adj h → ∀ x ∈ ℋ ∀ y ∈ ℋ adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y
8 dmadjrn ⊢ adj h ⁡ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T ∈ dom ⁡ adj h
9 dmadjop ⊢ adj h ⁡ adj h ⁡ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T : ℋ ⟶ ℋ
10 2 8 9 3syl ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T : ℋ ⟶ ℋ
11 dmadjop ⊢ T ∈ dom ⁡ adj h → T : ℋ ⟶ ℋ
12 hoeq1 ⊢ adj h ⁡ adj h ⁡ T : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ adj h ⁡ adj h ⁡ T = T
13 10 11 12 syl2anc ⊢ T ∈ dom ⁡ adj h → ∀ x ∈ ℋ ∀ y ∈ ℋ adj h ⁡ adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ adj h ⁡ adj h ⁡ T = T
14 7 13 mpbid ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T = T