Metamath Proof Explorer

Theorem adjbd1o

Description: The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjbd1o 
|- ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp

Proof

Step Hyp Ref Expression
1 adj1o 
 |-  adjh : dom adjh -1-1-onto-> dom adjh
2 f1of1 
 |-  ( adjh : dom adjh -1-1-onto-> dom adjh -> adjh : dom adjh -1-1-> dom adjh )
3 1 2 ax-mp 
 |-  adjh : dom adjh -1-1-> dom adjh
4 bdopssadj 
 |-  BndLinOp C_ dom adjh
5 f1ores 
 |-  ( ( adjh : dom adjh -1-1-> dom adjh /\ BndLinOp C_ dom adjh ) -> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) )
6 3 4 5 mp2an 
 |-  ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp )
7 vex 
 |-  y e. _V
8 7 elima 
 |-  ( y e. ( adjh " BndLinOp ) <-> E. x e. BndLinOp x adjh y )
9 f1ofn 
 |-  ( adjh : dom adjh -1-1-onto-> dom adjh -> adjh Fn dom adjh )
10 1 9 ax-mp 
 |-  adjh Fn dom adjh
11 bdopadj 
 |-  ( x e. BndLinOp -> x e. dom adjh )
12 fnbrfvb 
 |-  ( ( adjh Fn dom adjh /\ x e. dom adjh ) -> ( ( adjh ` x ) = y <-> x adjh y ) )
13 10 11 12 sylancr 
 |-  ( x e. BndLinOp -> ( ( adjh ` x ) = y <-> x adjh y ) )
14 13 rexbiia 
 |-  ( E. x e. BndLinOp ( adjh ` x ) = y <-> E. x e. BndLinOp x adjh y )
15 adjbdlnb 
 |-  ( x e. BndLinOp <-> ( adjh ` x ) e. BndLinOp )
16 eleq1 
 |-  ( ( adjh ` x ) = y -> ( ( adjh ` x ) e. BndLinOp <-> y e. BndLinOp ) )
17 15 16 syl5bb 
 |-  ( ( adjh ` x ) = y -> ( x e. BndLinOp <-> y e. BndLinOp ) )
18 17 biimpcd 
 |-  ( x e. BndLinOp -> ( ( adjh ` x ) = y -> y e. BndLinOp ) )
19 18 rexlimiv 
 |-  ( E. x e. BndLinOp ( adjh ` x ) = y -> y e. BndLinOp )
20 adjbdln 
 |-  ( y e. BndLinOp -> ( adjh ` y ) e. BndLinOp )
21 bdopadj 
 |-  ( y e. BndLinOp -> y e. dom adjh )
22 adjadj 
 |-  ( y e. dom adjh -> ( adjh ` ( adjh ` y ) ) = y )
23 21 22 syl 
 |-  ( y e. BndLinOp -> ( adjh ` ( adjh ` y ) ) = y )
24 fveqeq2 
 |-  ( x = ( adjh ` y ) -> ( ( adjh ` x ) = y <-> ( adjh ` ( adjh ` y ) ) = y ) )
25 24 rspcev 
 |-  ( ( ( adjh ` y ) e. BndLinOp /\ ( adjh ` ( adjh ` y ) ) = y ) -> E. x e. BndLinOp ( adjh ` x ) = y )
26 20 23 25 syl2anc 
 |-  ( y e. BndLinOp -> E. x e. BndLinOp ( adjh ` x ) = y )
27 19 26 impbii 
 |-  ( E. x e. BndLinOp ( adjh ` x ) = y <-> y e. BndLinOp )
28 8 14 27 3bitr2i 
 |-  ( y e. ( adjh " BndLinOp ) <-> y e. BndLinOp )
29 28 eqriv 
 |-  ( adjh " BndLinOp ) = BndLinOp
30 f1oeq3 
 |-  ( ( adjh " BndLinOp ) = BndLinOp -> ( ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) <-> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp ) )
31 29 30 ax-mp 
 |-  ( ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> ( adjh " BndLinOp ) <-> ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp )
32 6 31 mpbi 
 |-  ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp