This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℎ ↾ BndLinOp ) : BndLinOp –1-1-onto→ BndLinOp

Proof

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