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 \in LinFn \land {norm}_{fn} (T) \in ℝ) \to \exists! y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ T \in (LinFn \cap ContFn) \leftrightarrow (T \in LinFn \land T \in ContFn)$
2		lnfncnbd	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow {norm}_{fn} (T) \in ℝ)$
3	2	pm5.32i	$⊢ (T \in LinFn \land T \in ContFn) \leftrightarrow (T \in LinFn \land {norm}_{fn} (T) \in ℝ)$
4	1 3	bitri	$⊢ T \in (LinFn \cap ContFn) \leftrightarrow (T \in LinFn \land {norm}_{fn} (T) \in ℝ)$
5		riesz4	$⊢ T \in (LinFn \cap ContFn) \to \exists! y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$
6	4 5	sylbir	$⊢ (T \in LinFn \land {norm}_{fn} (T) \in ℝ) \to \exists! y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$

Metamath Proof Explorer

Theorem riesz2

Proof