Metamath Proof Explorer

Description: An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjbdlnb $⊢ T ∈ BndLinOp ↔ adj h ⁡ T ∈ BndLinOp$

Proof

Step Hyp Ref Expression
1 adjbdln $⊢ T ∈ BndLinOp → adj h ⁡ T ∈ BndLinOp$
2 bdopadj $⊢ adj h ⁡ T ∈ BndLinOp → adj h ⁡ T ∈ dom ⁡ adj h$
3 dmadjrnb $⊢ T ∈ dom ⁡ adj h ↔ adj h ⁡ T ∈ dom ⁡ adj h$
4 2 3 sylibr $⊢ adj h ⁡ T ∈ BndLinOp → T ∈ dom ⁡ adj h$
5 cnvadj $⊢ adj h -1 = adj h$
6 5 fveq1i $⊢ adj h -1 ⁡ adj h ⁡ T = adj h ⁡ adj h ⁡ T$
7 adj1o $⊢ adj h : dom ⁡ adj h ⟶ 1-1 onto dom ⁡ adj h$
8 simpl $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T ∈ BndLinOp → T ∈ dom ⁡ adj h$
9 f1ocnvfv1 $⊢ adj h : dom ⁡ adj h ⟶ 1-1 onto dom ⁡ adj h ∧ T ∈ dom ⁡ adj h → adj h -1 ⁡ adj h ⁡ T = T$
10 7 8 9 sylancr $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T ∈ BndLinOp → adj h -1 ⁡ adj h ⁡ T = T$
11 6 10 syl5eqr $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T ∈ BndLinOp → adj h ⁡ adj h ⁡ T = T$
12 adjbdln $⊢ adj h ⁡ T ∈ BndLinOp → adj h ⁡ adj h ⁡ T ∈ BndLinOp$
13 12 adantl $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T ∈ BndLinOp → adj h ⁡ adj h ⁡ T ∈ BndLinOp$
14 11 13 eqeltrrd $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T ∈ BndLinOp → T ∈ BndLinOp$
15 4 14 mpancom $⊢ adj h ⁡ T ∈ BndLinOp → T ∈ BndLinOp$
16 1 15 impbii $⊢ T ∈ BndLinOp ↔ adj h ⁡ T ∈ BndLinOp$