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