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