Metamath Proof Explorer


Theorem adjbdln

Description: The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjbdln
|- ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )

Proof

Step Hyp Ref Expression
1 bdopadj
 |-  ( T e. BndLinOp -> T e. dom adjh )
2 adjval
 |-  ( T e. dom adjh -> ( adjh ` T ) = ( iota_ t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
3 1 2 syl
 |-  ( T e. BndLinOp -> ( adjh ` T ) = ( iota_ t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
4 cnlnadj
 |-  ( T e. ( LinOp i^i ContOp ) -> E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
5 lncnopbd
 |-  ( T e. ( LinOp i^i ContOp ) <-> T e. BndLinOp )
6 lncnbd
 |-  ( LinOp i^i ContOp ) = BndLinOp
7 6 rexeqi
 |-  ( E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> E. t e. BndLinOp A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
8 4 5 7 3imtr3i
 |-  ( T e. BndLinOp -> E. t e. BndLinOp A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
9 bdopf
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
10 bdopf
 |-  ( t e. BndLinOp -> t : ~H --> ~H )
11 adjsym
 |-  ( ( T : ~H --> ~H /\ t : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( T ` x ) .ih y ) ) )
12 9 10 11 syl2an
 |-  ( ( T e. BndLinOp /\ t e. BndLinOp ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( T ` x ) .ih y ) ) )
13 eqcom
 |-  ( ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> ( x .ih ( t ` y ) ) = ( ( T ` x ) .ih y ) )
14 13 2ralbii
 |-  ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( T ` x ) .ih y ) )
15 12 14 bitr4di
 |-  ( ( T e. BndLinOp /\ t e. BndLinOp ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
16 15 rexbidva
 |-  ( T e. BndLinOp -> ( E. t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) <-> E. t e. BndLinOp A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
17 8 16 mpbird
 |-  ( T e. BndLinOp -> E. t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
18 adjeu
 |-  ( T : ~H --> ~H -> ( T e. dom adjh <-> E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
19 9 18 syl
 |-  ( T e. BndLinOp -> ( T e. dom adjh <-> E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
20 1 19 mpbid
 |-  ( T e. BndLinOp -> E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
21 ax-hilex
 |-  ~H e. _V
22 21 21 elmap
 |-  ( t e. ( ~H ^m ~H ) <-> t : ~H --> ~H )
23 10 22 sylibr
 |-  ( t e. BndLinOp -> t e. ( ~H ^m ~H ) )
24 23 ssriv
 |-  BndLinOp C_ ( ~H ^m ~H )
25 id
 |-  ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
26 25 rgenw
 |-  A. t e. BndLinOp ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
27 riotass2
 |-  ( ( ( BndLinOp C_ ( ~H ^m ~H ) /\ A. t e. BndLinOp ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) ) /\ ( E. t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) /\ E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) ) -> ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) = ( iota_ t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
28 24 26 27 mpanl12
 |-  ( ( E. t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) /\ E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) -> ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) = ( iota_ t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
29 17 20 28 syl2anc
 |-  ( T e. BndLinOp -> ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) = ( iota_ t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
30 3 29 eqtr4d
 |-  ( T e. BndLinOp -> ( adjh ` T ) = ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
31 24 a1i
 |-  ( T e. BndLinOp -> BndLinOp C_ ( ~H ^m ~H ) )
32 reuss
 |-  ( ( BndLinOp C_ ( ~H ^m ~H ) /\ E. t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) /\ E! t e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) -> E! t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
33 31 17 20 32 syl3anc
 |-  ( T e. BndLinOp -> E! t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
34 riotacl
 |-  ( E! t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) -> ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) e. BndLinOp )
35 33 34 syl
 |-  ( T e. BndLinOp -> ( iota_ t e. BndLinOp A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) e. BndLinOp )
36 30 35 eqeltrd
 |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )