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

Metamath Proof Explorer

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 )