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

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
7 vex 3176 . . . . . 6 𝑦 ∈ V
87elima 5390 . . . . 5 (𝑦 ∈ (adj “ BndLinOp) ↔ ∃𝑥 ∈ BndLinOp 𝑥adj𝑦)
101, 9ax-mp 5 . . . . . . 7 adj Fn dom adj
11 bdopadj 28325 . . . . . . 7 (𝑥 ∈ BndLinOp → 𝑥 ∈ dom adj)
1310, 11, 12sylancr 694 . . . . . 6 (𝑥 ∈ BndLinOp → ((adj𝑥) = 𝑦𝑥adj𝑦))
1413rexbiia 3022 . . . . 5 (∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦 ↔ ∃𝑥 ∈ BndLinOp 𝑥adj𝑦)
15 adjbdlnb 28327 . . . . . . . . 9 (𝑥 ∈ BndLinOp ↔ (adj𝑥) ∈ BndLinOp)
16 eleq1 2676 . . . . . . . . 9 ((adj𝑥) = 𝑦 → ((adj𝑥) ∈ BndLinOp ↔ 𝑦 ∈ BndLinOp))
1715, 16syl5bb 271 . . . . . . . 8 ((adj𝑥) = 𝑦 → (𝑥 ∈ BndLinOp ↔ 𝑦 ∈ BndLinOp))
1817biimpcd 238 . . . . . . 7 (𝑥 ∈ BndLinOp → ((adj𝑥) = 𝑦𝑦 ∈ BndLinOp))
1918rexlimiv 3009 . . . . . 6 (∃𝑥 ∈ BndLinOp (adj𝑥) = 𝑦𝑦 ∈ BndLinOp)
20 adjbdln 28326 . . . . . . 7 (𝑦 ∈ BndLinOp → (adj𝑦) ∈ BndLinOp)
21 bdopadj 28325 . . . . . . . 8 (𝑦 ∈ BndLinOp → 𝑦 ∈ dom adj)