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 ontoBndLinOp

Proof

Step Hyp Ref Expression
1 adj1o ⊢adjh:dom⁡adjh⟶1-1 ontodom⁡adjh
2 f1of1 ⊢adjh:dom⁡adjh⟶1-1 ontodom⁡adjh→adjh:dom⁡adjh⟶1-1dom⁡adjh
3 1 2 ax-mp ⊢adjh:dom⁡adjh⟶1-1dom⁡adjh
4 bdopssadj ⊢BndLinOp⊆dom⁡adjh
5 f1ores ⊢adjh:dom⁡adjh⟶1-1dom⁡adjh∧BndLinOp⊆dom⁡adjh→adjh↾BndLinOp:BndLinOp⟶1-1 ontoadjhBndLinOp
6 3 4 5 mp2an ⊢adjh↾BndLinOp:BndLinOp⟶1-1 ontoadjhBndLinOp
7 vex ⊢y∈V
8 7 elima ⊢y∈adjhBndLinOp↔∃x∈BndLinOpxadjhy
9 f1ofn ⊢adjh:dom⁡adjh⟶1-1 ontodom⁡adjh→adjhFndom⁡adjh
10 1 9 ax-mp ⊢adjhFndom⁡adjh
11 bdopadj ⊢x∈BndLinOp→x∈dom⁡adjh
12 fnbrfvb ⊢adjhFndom⁡adjh∧x∈dom⁡adjh→adjh⁡x=y↔xadjhy
13 10 11 12 sylancr ⊢x∈BndLinOp→adjh⁡x=y↔xadjhy
14 13 rexbiia ⊢∃x∈BndLinOpadjh⁡x=y↔∃x∈BndLinOpxadjhy
15 adjbdlnb ⊢x∈BndLinOp↔adjh⁡x∈BndLinOp
16 eleq1 ⊢adjh⁡x=y→adjh⁡x∈BndLinOp↔y∈BndLinOp
17 15 16 bitrid ⊢adjh⁡x=y→x∈BndLinOp↔y∈BndLinOp
18 17 biimpcd ⊢x∈BndLinOp→adjh⁡x=y→y∈BndLinOp
19 18 rexlimiv ⊢∃x∈BndLinOpadjh⁡x=y→y∈BndLinOp
20 adjbdln ⊢y∈BndLinOp→adjh⁡y∈BndLinOp
21 bdopadj ⊢y∈BndLinOp→y∈dom⁡adjh
22 adjadj ⊢y∈dom⁡adjh→adjh⁡adjh⁡y=y
23 21 22 syl ⊢y∈BndLinOp→adjh⁡adjh⁡y=y
24 fveqeq2 ⊢x=adjh⁡y→adjh⁡x=y↔adjh⁡adjh⁡y=y
25 24 rspcev ⊢adjh⁡y∈BndLinOp∧adjh⁡adjh⁡y=y→∃x∈BndLinOpadjh⁡x=y
26 20 23 25 syl2anc ⊢y∈BndLinOp→∃x∈BndLinOpadjh⁡x=y
27 19 26 impbii ⊢∃x∈BndLinOpadjh⁡x=y↔y∈BndLinOp
28 8 14 27 3bitr2i ⊢y∈adjhBndLinOp↔y∈BndLinOp
29 28 eqriv ⊢adjhBndLinOp=BndLinOp
30 f1oeq3 ⊢adjhBndLinOp=BndLinOp→adjh↾BndLinOp:BndLinOp⟶1-1 ontoadjhBndLinOp↔adjh↾BndLinOp:BndLinOp⟶1-1 ontoBndLinOp
31 29 30 ax-mp ⊢adjh↾BndLinOp:BndLinOp⟶1-1 ontoadjhBndLinOp↔adjh↾BndLinOp:BndLinOp⟶1-1 ontoBndLinOp
32 6 31 mpbi ⊢adjh↾BndLinOp:BndLinOp⟶1-1 ontoBndLinOp