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

Metamath Proof Explorer

Theorem cnlnadjlem3

Description: Lemma for cnlnadji . By riesz4 , B is the unique vector such that ( Tv ) .ih y ) = ( v .ih w ) for all v . (Contributed by NM, 17-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 ) )
Assertion cnlnadjlem3 
|- ( y e. ~H -> B e. ~H )

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 1 2 3 cnlnadjlem2 
 |-  ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )
6 elin 
 |-  ( G e. ( LinFn i^i ContFn ) <-> ( G e. LinFn /\ G e. ContFn ) )
7 5 6 sylibr 
 |-  ( y e. ~H -> G e. ( LinFn i^i ContFn ) )
8 riesz4 
 |-  ( G e. ( LinFn i^i ContFn ) -> E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) )
9 7 8 syl 
 |-  ( y e. ~H -> E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) )
10 1 2 3 cnlnadjlem1 
 |-  ( v e. ~H -> ( G ` v ) = ( ( T ` v ) .ih y ) )
11 10 eqeq1d 
 |-  ( v e. ~H -> ( ( G ` v ) = ( v .ih w ) <-> ( ( T ` v ) .ih y ) = ( v .ih w ) ) )
12 11 ralbiia 
 |-  ( A. v e. ~H ( G ` v ) = ( v .ih w ) <-> A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
13 12 reubii 
 |-  ( E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) <-> E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
14 9 13 sylib 
 |-  ( y e. ~H -> E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
15 riotacl 
 |-  ( E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) -> ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) e. ~H )
16 14 15 syl 
 |-  ( y e. ~H -> ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) e. ~H )
17 4 16 eqeltrid 
 |-  ( y e. ~H -> B e. ~H )