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

Metamath Proof Explorer

Theorem riesz2

Description: Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of Halmos p. 31. For part 1, see riesz1 . (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion riesz2 
|- ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( T e. ( LinFn i^i ContFn ) <-> ( T e. LinFn /\ T e. ContFn ) )
2 lnfncnbd 
 |-  ( T e. LinFn -> ( T e. ContFn <-> ( normfn ` T ) e. RR ) )
3 2 pm5.32i 
 |-  ( ( T e. LinFn /\ T e. ContFn ) <-> ( T e. LinFn /\ ( normfn ` T ) e. RR ) )
4 1 3 bitri 
 |-  ( T e. ( LinFn i^i ContFn ) <-> ( T e. LinFn /\ ( normfn ` T ) e. RR ) )
5 riesz4 
 |-  ( T e. ( LinFn i^i ContFn ) -> E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )
6 4 5 sylbir 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )