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 )