Metamath Proof Explorer

Theorem cnlnssadj

Description: Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnlnssadj 
|- ( LinOp i^i ContOp ) C_ dom adjh

Proof

Step Hyp Ref Expression
1 cnlnadj 
 |-  ( y e. ( LinOp i^i ContOp ) -> E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) )
2 df-rex 
 |-  ( E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) <-> E. t ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) )
3 1 2 sylib 
 |-  ( y e. ( LinOp i^i ContOp ) -> E. t ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) )
4 inss1 
 |-  ( LinOp i^i ContOp ) C_ LinOp
5 4 sseli 
 |-  ( y e. ( LinOp i^i ContOp ) -> y e. LinOp )
6 lnopf 
 |-  ( y e. LinOp -> y : ~H --> ~H )
7 5 6 syl 
 |-  ( y e. ( LinOp i^i ContOp ) -> y : ~H --> ~H )
8 7 a1d 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> y : ~H --> ~H ) )
9 4 sseli 
 |-  ( t e. ( LinOp i^i ContOp ) -> t e. LinOp )
10 lnopf 
 |-  ( t e. LinOp -> t : ~H --> ~H )
11 9 10 syl 
 |-  ( t e. ( LinOp i^i ContOp ) -> t : ~H --> ~H )
12 11 a1i 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( t e. ( LinOp i^i ContOp ) -> t : ~H --> ~H ) )
13 12 adantrd 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> t : ~H --> ~H ) )
14 eqcom 
 |-  ( ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) <-> ( x .ih ( t ` z ) ) = ( ( y ` x ) .ih z ) )
15 14 biimpi 
 |-  ( ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) -> ( x .ih ( t ` z ) ) = ( ( y ` x ) .ih z ) )
16 15 2ralimi 
 |-  ( A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) -> A. x e. ~H A. z e. ~H ( x .ih ( t ` z ) ) = ( ( y ` x ) .ih z ) )
17 adjsym 
 |-  ( ( t : ~H --> ~H /\ y : ~H --> ~H ) -> ( A. x e. ~H A. z e. ~H ( x .ih ( t ` z ) ) = ( ( y ` x ) .ih z ) <-> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
18 11 7 17 syl2anr 
 |-  ( ( y e. ( LinOp i^i ContOp ) /\ t e. ( LinOp i^i ContOp ) ) -> ( A. x e. ~H A. z e. ~H ( x .ih ( t ` z ) ) = ( ( y ` x ) .ih z ) <-> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
19 16 18 imbitrid 
 |-  ( ( y e. ( LinOp i^i ContOp ) /\ t e. ( LinOp i^i ContOp ) ) -> ( A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) -> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
20 19 expimpd 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
21 8 13 20 3jcad 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> ( y : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) ) )
22 dfadj2 
 |-  adjh = { <. u , v >. | ( u : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) ) }
23 22 eleq2i 
 |-  ( <. y , t >. e. adjh <-> <. y , t >. e. { <. u , v >. | ( u : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) ) } )
24 vex 
 |-  y e. _V
25 vex 
 |-  t e. _V
26 feq1 
 |-  ( u = y -> ( u : ~H --> ~H <-> y : ~H --> ~H ) )
27 fveq1 
 |-  ( u = y -> ( u ` z ) = ( y ` z ) )
28 27 oveq2d 
 |-  ( u = y -> ( x .ih ( u ` z ) ) = ( x .ih ( y ` z ) ) )
29 28 eqeq1d 
 |-  ( u = y -> ( ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) <-> ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) ) )
30 29 2ralbidv 
 |-  ( u = y -> ( A. x e. ~H A. z e. ~H ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) <-> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) ) )
31 26 30 3anbi13d 
 |-  ( u = y -> ( ( u : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) ) <-> ( y : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) ) ) )
32 feq1 
 |-  ( v = t -> ( v : ~H --> ~H <-> t : ~H --> ~H ) )
33 fveq1 
 |-  ( v = t -> ( v ` x ) = ( t ` x ) )
34 33 oveq1d 
 |-  ( v = t -> ( ( v ` x ) .ih z ) = ( ( t ` x ) .ih z ) )
35 34 eqeq2d 
 |-  ( v = t -> ( ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) <-> ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
36 35 2ralbidv 
 |-  ( v = t -> ( A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) <-> A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
37 32 36 3anbi23d 
 |-  ( v = t -> ( ( y : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( v ` x ) .ih z ) ) <-> ( y : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) ) )
38 24 25 31 37 opelopab 
 |-  ( <. y , t >. e. { <. u , v >. | ( u : ~H --> ~H /\ v : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( u ` z ) ) = ( ( v ` x ) .ih z ) ) } <-> ( y : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) )
39 23 38 bitr2i 
 |-  ( ( y : ~H --> ~H /\ t : ~H --> ~H /\ A. x e. ~H A. z e. ~H ( x .ih ( y ` z ) ) = ( ( t ` x ) .ih z ) ) <-> <. y , t >. e. adjh )
40 21 39 imbitrdi 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> <. y , t >. e. adjh ) )
41 40 eximdv 
 |-  ( y e. ( LinOp i^i ContOp ) -> ( E. t ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( y ` x ) .ih z ) = ( x .ih ( t ` z ) ) ) -> E. t <. y , t >. e. adjh ) )
42 3 41 mpd 
 |-  ( y e. ( LinOp i^i ContOp ) -> E. t <. y , t >. e. adjh )
43 24 eldm2 
 |-  ( y e. dom adjh <-> E. t <. y , t >. e. adjh )
44 42 43 sylibr 
 |-  ( y e. ( LinOp i^i ContOp ) -> y e. dom adjh )
45 44 ssriv 
 |-  ( LinOp i^i ContOp ) C_ dom adjh