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