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