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 e. BndLinOp <-> ( adjh ` T ) e. BndLinOp )

Proof

Step Hyp Ref Expression
1 adjbdln 
 |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
2 bdopadj 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) e. dom adjh )
3 dmadjrnb 
 |-  ( T e. dom adjh <-> ( adjh ` T ) e. dom adjh )
4 2 3 sylibr 
 |-  ( ( adjh ` T ) e. BndLinOp -> T e. dom adjh )
5 cnvadj 
 |-  `' adjh = adjh
6 5 fveq1i 
 |-  ( `' adjh ` ( adjh ` T ) ) = ( adjh ` ( adjh ` T ) )
7 adj1o 
 |-  adjh : dom adjh -1-1-onto-> dom adjh
8 simpl 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. BndLinOp ) -> T e. dom adjh )
9 f1ocnvfv1 
 |-  ( ( adjh : dom adjh -1-1-onto-> dom adjh /\ T e. dom adjh ) -> ( `' adjh ` ( adjh ` T ) ) = T )
10 7 8 9 sylancr 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. BndLinOp ) -> ( `' adjh ` ( adjh ` T ) ) = T )
11 6 10 eqtr3id 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. BndLinOp ) -> ( adjh ` ( adjh ` T ) ) = T )
12 adjbdln 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` ( adjh ` T ) ) e. BndLinOp )
13 12 adantl 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. BndLinOp ) -> ( adjh ` ( adjh ` T ) ) e. BndLinOp )
14 11 13 eqeltrrd 
 |-  ( ( T e. dom adjh /\ ( adjh ` T ) e. BndLinOp ) -> T e. BndLinOp )
15 4 14 mpancom 
 |-  ( ( adjh ` T ) e. BndLinOp -> T e. BndLinOp )
16 1 15 impbii 
 |-  ( T e. BndLinOp <-> ( adjh ` T ) e. BndLinOp )