Theorem adjbdlnb

Description: An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjbdlnb	⊢ ( 𝑇 ∈ BndLinOp ↔ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )

Proof

Step	Hyp	Ref	Expression
1		adjbdln	⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )
2		bdopadj	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
3		dmadjrnb	⊢ ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
4	2 3	sylibr	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → 𝑇 ∈ dom adjℎ )
5		cnvadj	⊢ ◡ adjℎ = adjℎ
6	5	fveq1i	⊢ ( ◡ adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) )
7		adj1o	⊢ adjℎ : dom adjℎ –1-1-onto→ dom adjℎ
8		simpl	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) → 𝑇 ∈ dom adjℎ )
9		f1ocnvfv1	⊢ ( ( adjℎ : dom adjℎ –1-1-onto→ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( ◡ adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
10	7 8 9	sylancr	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) → ( ◡ adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
11	6 10	eqtr3id	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
12		adjbdln	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) ∈ BndLinOp )
13	12	adantl	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) ∈ BndLinOp )
14	11 13	eqeltrrd	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) → 𝑇 ∈ BndLinOp )
15	4 14	mpancom	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → 𝑇 ∈ BndLinOp )
16	1 15	impbii	⊢ ( 𝑇 ∈ BndLinOp ↔ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )