This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnlnadji

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
Hypotheses cnlnadj.1 
|- T e. LinOp
cnlnadj.2 
|- T e. ContOp
Assertion cnlnadji 
|- 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 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 ) )