Metamath Proof Explorer

Theorem cnlnadjeui

Description: Every continuous linear operator has a unique adjoint. Theorem 3.10 of Beran p. 104. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadj.1 
|- T e. LinOp
cnlnadj.2 
|- T e. ContOp
Assertion cnlnadjeui 
|- E! t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )

Proof

Step Hyp Ref Expression
1 cnlnadj.1 
 |-  T e. LinOp
2 cnlnadj.2 
 |-  T e. ContOp
3 1 2 cnlnadji 
 |-  E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )
4 adjmo 
 |-  E* t ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) )
5 inss1 
 |-  ( LinOp i^i ContOp ) C_ LinOp
6 5 sseli 
 |-  ( t e. ( LinOp i^i ContOp ) -> t e. LinOp )
7 lnopf 
 |-  ( t e. LinOp -> t : ~H --> ~H )
8 6 7 syl 
 |-  ( t e. ( LinOp i^i ContOp ) -> t : ~H --> ~H )
9 simpl 
 |-  ( ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) -> t : ~H --> ~H )
10 eqcom 
 |-  ( ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> ( x .ih ( t ` y ) ) = ( ( T ` x ) .ih y ) )
11 10 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 ) )
12 1 lnopfi 
 |-  T : ~H --> ~H
13 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 ) ) )
14 12 13 mpan2 
 |-  ( 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 ) ) )
15 11 14 bitrid 
 |-  ( t : ~H --> ~H -> ( 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 ) ) )
16 15 biimpa 
 |-  ( ( t : ~H --> ~H /\ 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 ) )
17 9 16 jca 
 |-  ( ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) -> ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
18 8 17 sylan 
 |-  ( ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) -> ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) )
19 18 moimi 
 |-  ( E* t ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) -> E* t ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
20 df-rmo 
 |-  ( 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 ( t e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
21 19 20 sylibr 
 |-  ( E* t ( t : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( t ` x ) .ih y ) ) -> E* t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
22 4 21 ax-mp 
 |-  E* t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )
23 reu5 
 |-  ( 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. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) /\ E* t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
24 3 22 23 mpbir2an 
 |-  E! t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )