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 ) )