Metamath Proof Explorer

Theorem cnlnadjeu

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

Ref Expression
Assertion cnlnadjeu 
|- ( 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 ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) -> ( T ` x ) = ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) )
2 1 oveq1d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) -> ( ( T ` x ) .ih y ) = ( ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) .ih y ) )
3 2 eqeq1d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) -> ( ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> ( ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
4 3 2ralbidv 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) -> ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) <-> A. x e. ~H A. y e. ~H ( ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
5 4 reubidv 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) -> ( 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 ( ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) .ih y ) = ( x .ih ( t ` y ) ) ) )
6 inss1 
 |-  ( LinOp i^i ContOp ) C_ LinOp
7 0lnop 
 |-  0hop e. LinOp
8 0cnop 
 |-  0hop e. ContOp
9 elin 
 |-  ( 0hop e. ( LinOp i^i ContOp ) <-> ( 0hop e. LinOp /\ 0hop e. ContOp ) )
10 7 8 9 mpbir2an 
 |-  0hop e. ( LinOp i^i ContOp )
11 10 elimel 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) e. ( LinOp i^i ContOp )
12 6 11 sselii 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) e. LinOp
13 inss2 
 |-  ( LinOp i^i ContOp ) C_ ContOp
14 13 11 sselii 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) e. ContOp
15 12 14 cnlnadjeui 
 |-  E! t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( if ( T e. ( LinOp i^i ContOp ) , T , 0hop ) ` x ) .ih y ) = ( x .ih ( t ` y ) )
16 5 15 dedth 
 |-  ( 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 ) ) )