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	⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) )
2		lnfncnbd	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ( normfn ‘ 𝑇 ) ∈ ℝ ) )
3	2	pm5.32i	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) )
4	1 3	bitri	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) )
5		riesz4	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
6	4 5	sylbir	⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )