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 ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → ∃! y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y

Proof

Step Hyp Ref Expression
1 elin ⊢ T ∈ LinFn ∩ ContFn ↔ T ∈ LinFn ∧ T ∈ ContFn
2 lnfncnbd ⊢ T ∈ LinFn → T ∈ ContFn ↔ norm fn ⁡ T ∈ ℝ
3 2 pm5.32i ⊢ T ∈ LinFn ∧ T ∈ ContFn ↔ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ
4 1 3 bitri ⊢ T ∈ LinFn ∩ ContFn ↔ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ
5 riesz4 ⊢ T ∈ LinFn ∩ ContFn → ∃! y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
6 4 5 sylbir ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → ∃! y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y