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 TBndLinOpadjhTBndLinOp

Proof

Step Hyp Ref Expression
1 adjbdln TBndLinOpadjhTBndLinOp
2 bdopadj adjhTBndLinOpadjhTdomadjh
3 dmadjrnb TdomadjhadjhTdomadjh
4 2 3 sylibr adjhTBndLinOpTdomadjh
5 cnvadj adjh-1=adjh
6 5 fveq1i adjh-1adjhT=adjhadjhT
7 adj1o adjh:domadjh1-1 ontodomadjh
8 simpl TdomadjhadjhTBndLinOpTdomadjh
9 f1ocnvfv1 adjh:domadjh1-1 ontodomadjhTdomadjhadjh-1adjhT=T
10 7 8 9 sylancr TdomadjhadjhTBndLinOpadjh-1adjhT=T
11 6 10 eqtr3id TdomadjhadjhTBndLinOpadjhadjhT=T
12 adjbdln adjhTBndLinOpadjhadjhTBndLinOp
13 12 adantl TdomadjhadjhTBndLinOpadjhadjhTBndLinOp
14 11 13 eqeltrrd TdomadjhadjhTBndLinOpTBndLinOp
15 4 14 mpancom adjhTBndLinOpTBndLinOp
16 1 15 impbii TBndLinOpadjhTBndLinOp