# Metamath Proof Explorer

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

Ref Expression
`|- T e. LinOp`
`|- T e. 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
` |-  T e. LinOp`
` |-  T e. ContOp`
3 eqid
` |-  ( g e. ~H |-> ( ( T ` g ) .ih z ) ) = ( g e. ~H |-> ( ( T ` g ) .ih z ) )`
4 oveq2
` |-  ( f = w -> ( v .ih f ) = ( v .ih w ) )`
5 4 eqeq2d
` |-  ( f = w -> ( ( ( T ` v ) .ih z ) = ( v .ih f ) <-> ( ( T ` v ) .ih z ) = ( v .ih w ) ) )`
6 5 ralbidv
` |-  ( f = w -> ( A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) <-> A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih w ) ) )`
7 6 cbvriotavw
` |-  ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih w ) )`
8 eqid
` |-  ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) = ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) )`
9 1 2 3 7 8 cnlnadjlem9
` |-  E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )`