Metamath Proof Explorer

Theorem cnlnadjlem9

Description: Lemma for cnlnadji . F provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 
|- T e. LinOp
cnlnadjlem.2 
|- T e. ContOp
cnlnadjlem.3 
|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
cnlnadjlem.4 
|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
cnlnadjlem.5 
|- F = ( y e. ~H |-> B )
Assertion cnlnadjlem9 
|- E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) )

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 
 |-  T e. LinOp
2 cnlnadjlem.2 
 |-  T e. ContOp
3 cnlnadjlem.3 
 |-  G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4 cnlnadjlem.4 
 |-  B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5 cnlnadjlem.5 
 |-  F = ( y e. ~H |-> B )
6 1 2 3 4 5 cnlnadjlem6 
 |-  F e. LinOp
7 1 2 3 4 5 cnlnadjlem8 
 |-  F e. ContOp
8 elin 
 |-  ( F e. ( LinOp i^i ContOp ) <-> ( F e. LinOp /\ F e. ContOp ) )
9 6 7 8 mpbir2an 
 |-  F e. ( LinOp i^i ContOp )
10 1 2 3 4 5 cnlnadjlem5 
 |-  ( ( z e. ~H /\ x e. ~H ) -> ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) ) )
11 10 ancoms 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) ) )
12 11 rgen2 
 |-  A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) )
13 fveq1 
 |-  ( t = F -> ( t ` z ) = ( F ` z ) )
14 13 oveq2d 
 |-  ( t = F -> ( x .ih ( t ` z ) ) = ( x .ih ( F ` z ) ) )
15 14 eqeq2d 
 |-  ( t = F -> ( ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) ) <-> ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) ) ) )
16 15 2ralbidv 
 |-  ( t = F -> ( A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) ) <-> A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) ) ) )
17 16 rspcev 
 |-  ( ( F e. ( LinOp i^i ContOp ) /\ A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( F ` z ) ) ) -> E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) ) )
18 9 12 17 mp2an 
 |-  E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) )