Metamath Proof Explorer

Theorem adjbdlnb

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 eqtr3id ⊢ 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