# Metamath Proof Explorer

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
`|- ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )`

### Proof

Step Hyp Ref Expression
` |-  ( T e. BndLinOp -> T e. dom adjh )`
` |-  ( 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 ) ) )`
` |-  ( 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 )`
` |-  ( ( 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 syl6bbr
` |-  ( ( 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 ) )`
` |-  ( 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 )`