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 ⊢ adj h ↾ BndLinOp : BndLinOp ⟶ 1-1 onto BndLinOp

Proof

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