Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  adjbd1o Structured version   Visualization version   GIF version

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

Proof of Theorem adjbd1o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
4 bdopssadj 28786 . . 3 BndLinOp ⊆ dom adj
5 f1ores 6108 . . 3 ((adj:dom adj1-1→dom adj ∧ BndLinOp ⊆ dom adj) → (adj ↾ BndLinOp):BndLinOp–1-1-onto→(adj “ BndLinOp))
63, 4, 5mp2an 707 . 2 (adj ↾ BndLinOp):BndLinOp–1-1-onto→(adj “ BndLinOp)
7 vex 3189 . . . . . 6 𝑦 ∈ V
87elima 5430 . . . . 5 (𝑦 ∈ (adj “ BndLinOp) ↔ ∃𝑥 ∈ BndLinOp 𝑥adj𝑦)
9 f1ofn 6095 . . . . . . . 8 (adj:dom adj1-1-onto→dom adj → adj Fn dom adj)
101, 9ax-mp 5 . . . . . . 7 adj Fn dom adj
11 bdopadj 28787 . . . . . . 7 (𝑥 ∈ BndLinOp → 𝑥 ∈ dom adj)
12 fnbrfvb 6193 . . . . . . 7 ((adj Fn dom adj𝑥 ∈ dom adj) → ((adj𝑥) = 𝑦𝑥adj𝑦))
1310, 11, 12sylancr 694 . . . . . 6 (𝑥 ∈ BndLinOp → ((adj𝑥) = 𝑦𝑥adj𝑦))
1413rexbiia 3033 . . . . 5 (∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦 ↔ ∃𝑥 ∈ BndLinOp 𝑥adj𝑦)
15 adjbdlnb 28789 . . . . . . . . 9 (𝑥 ∈ BndLinOp ↔ (adj𝑥) ∈ BndLinOp)
16 eleq1 2686 . . . . . . . . 9 ((adj𝑥) = 𝑦 → ((adj𝑥) ∈ BndLinOp ↔ 𝑦 ∈ BndLinOp))
1715, 16syl5bb 272 . . . . . . . 8 ((adj𝑥) = 𝑦 → (𝑥 ∈ BndLinOp ↔ 𝑦 ∈ BndLinOp))
1817biimpcd 239 . . . . . . 7 (𝑥 ∈ BndLinOp → ((adj𝑥) = 𝑦𝑦 ∈ BndLinOp))
1918rexlimiv 3020 . . . . . 6 (∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦𝑦 ∈ BndLinOp)
20 adjbdln 28788 . . . . . . 7 (𝑦 ∈ BndLinOp → (adj𝑦) ∈ BndLinOp)
21 bdopadj 28787 . . . . . . . 8 (𝑦 ∈ BndLinOp → 𝑦 ∈ dom adj)
22 adjadj 28641 . . . . . . . 8 (𝑦 ∈ dom adj → (adj‘(adj𝑦)) = 𝑦)
2321, 22syl 17 . . . . . . 7 (𝑦 ∈ BndLinOp → (adj‘(adj𝑦)) = 𝑦)
24 fveq2 6148 . . . . . . . . 9 (𝑥 = (adj𝑦) → (adj𝑥) = (adj‘(adj𝑦)))
2524eqeq1d 2623 . . . . . . . 8 (𝑥 = (adj𝑦) → ((adj𝑥) = 𝑦 ↔ (adj‘(adj𝑦)) = 𝑦))
2625rspcev 3295 . . . . . . 7 (((adj𝑦) ∈ BndLinOp ∧ (adj‘(adj𝑦)) = 𝑦) → ∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦)
2720, 23, 26syl2anc 692 . . . . . 6 (𝑦 ∈ BndLinOp → ∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦)
2819, 27impbii 199 . . . . 5 (∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦𝑦 ∈ BndLinOp)
298, 14, 283bitr2i 288 . . . 4 (𝑦 ∈ (adj “ BndLinOp) ↔ 𝑦 ∈ BndLinOp)
3029eqriv 2618 . . 3 (adj “ BndLinOp) = BndLinOp
31 f1oeq3 6086 . . 3 ((adj “ BndLinOp) = BndLinOp → ((adj ↾ BndLinOp):BndLinOp–1-1-onto→(adj “ BndLinOp) ↔ (adj ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp))
3230, 31ax-mp 5 . 2 ((adj ↾ BndLinOp):BndLinOp–1-1-onto→(adj “ BndLinOp) ↔ (adj ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp)
336, 32mpbi 220 1 (adj ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp