riesz1

Description: Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of Halmos p. 31. For part 2, see riesz2 . For the continuous linear functional version, see riesz3i and riesz4 . (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	riesz1	$⊢ T \in LinFn \to ({norm}_{fn} (T) \in ℝ \leftrightarrow \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y)$

Proof

Step	Hyp	Ref	Expression
1		lnfncnbd	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow {norm}_{fn} (T) \in ℝ)$
2		elin	$⊢ T \in (LinFn \cap ContFn) \leftrightarrow (T \in LinFn \land T \in ContFn)$
3		fveq1	$⊢ T = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \to T (x) = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) (x)$
4	3	eqeq1d	$⊢ T = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \to (T (x) = x \cdot_{ih} y \leftrightarrow if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) (x) = x \cdot_{ih} y)$
5	4	rexralbidv	$⊢ T = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \to (\exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y \leftrightarrow \exists y \in ℋ \forall x \in ℋ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) (x) = x \cdot_{ih} y)$
6		inss1	$⊢ LinFn \cap ContFn \subseteq LinFn$
7		0lnfn	$⊢ ℋ \times \{0\} \in LinFn$
8		0cnfn	$⊢ ℋ \times \{0\} \in ContFn$
9		elin	$⊢ ℋ \times \{0\} \in (LinFn \cap ContFn) \leftrightarrow (ℋ \times \{0\} \in LinFn \land ℋ \times \{0\} \in ContFn)$
10	7 8 9	mpbir2an	$⊢ ℋ \times \{0\} \in (LinFn \cap ContFn)$
11	10	elimel	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in (LinFn \cap ContFn)$
12	6 11	sselii	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in LinFn$
13		inss2	$⊢ LinFn \cap ContFn \subseteq ContFn$
14	13 11	sselii	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in ContFn$
15	12 14	riesz3i	$⊢ \exists y \in ℋ \forall x \in ℋ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) (x) = x \cdot_{ih} y$
16	5 15	dedth	$⊢ T \in (LinFn \cap ContFn) \to \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$
17	2 16	sylbir	$⊢ (T \in LinFn \land T \in ContFn) \to \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y$
18	17	ex	$⊢ T \in LinFn \to (T \in ContFn \to \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y)$
19		normcl	$⊢ y \in ℋ \to {norm}_{ℎ} (y) \in ℝ$
20	19	adantl	$⊢ (T \in LinFn \land y \in ℋ) \to {norm}_{ℎ} (y) \in ℝ$
21		fveq2	$⊢ T (x) = x \cdot_{ih} y \to \|T (x)\| = \|x \cdot_{ih} y\|$
22	21	adantl	$⊢ (((T \in LinFn \land x \in ℋ) \land y \in ℋ) \land T (x) = x \cdot_{ih} y) \to \|T (x)\| = \|x \cdot_{ih} y\|$
23		bcs	$⊢ (x \in ℋ \land y \in ℋ) \to \|x \cdot_{ih} y\| \leq {norm}_{ℎ} (x) {norm}_{ℎ} (y)$
24		normcl	$⊢ x \in ℋ \to {norm}_{ℎ} (x) \in ℝ$
25		recn	$⊢ {norm}_{ℎ} (x) \in ℝ \to {norm}_{ℎ} (x) \in ℂ$
26		recn	$⊢ {norm}_{ℎ} (y) \in ℝ \to {norm}_{ℎ} (y) \in ℂ$
27		mulcom	$⊢ ({norm}_{ℎ} (x) \in ℂ \land {norm}_{ℎ} (y) \in ℂ) \to {norm}_{ℎ} (x) {norm}_{ℎ} (y) = {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
28	25 26 27	syl2an	$⊢ ({norm}_{ℎ} (x) \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to {norm}_{ℎ} (x) {norm}_{ℎ} (y) = {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
29	24 19 28	syl2an	$⊢ (x \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (x) {norm}_{ℎ} (y) = {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
30	23 29	breqtrd	$⊢ (x \in ℋ \land y \in ℋ) \to \|x \cdot_{ih} y\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
31	30	adantll	$⊢ ((T \in LinFn \land x \in ℋ) \land y \in ℋ) \to \|x \cdot_{ih} y\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
32	31	adantr	$⊢ (((T \in LinFn \land x \in ℋ) \land y \in ℋ) \land T (x) = x \cdot_{ih} y) \to \|x \cdot_{ih} y\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
33	22 32	eqbrtrd	$⊢ (((T \in LinFn \land x \in ℋ) \land y \in ℋ) \land T (x) = x \cdot_{ih} y) \to \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
34	33	ex	$⊢ ((T \in LinFn \land x \in ℋ) \land y \in ℋ) \to (T (x) = x \cdot_{ih} y \to \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x))$
35	34	an32s	$⊢ ((T \in LinFn \land y \in ℋ) \land x \in ℋ) \to (T (x) = x \cdot_{ih} y \to \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x))$
36	35	ralimdva	$⊢ (T \in LinFn \land y \in ℋ) \to (\forall x \in ℋ T (x) = x \cdot_{ih} y \to \forall x \in ℋ \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x))$
37		oveq1	$⊢ z = {norm}_{ℎ} (y) \to z {norm}_{ℎ} (x) = {norm}_{ℎ} (y) {norm}_{ℎ} (x)$
38	37	breq2d	$⊢ z = {norm}_{ℎ} (y) \to (\|T (x)\| \leq z {norm}_{ℎ} (x) \leftrightarrow \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x))$
39	38	ralbidv	$⊢ z = {norm}_{ℎ} (y) \to (\forall x \in ℋ \|T (x)\| \leq z {norm}_{ℎ} (x) \leftrightarrow \forall x \in ℋ \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x))$
40	39	rspcev	$⊢ ({norm}_{ℎ} (y) \in ℝ \land \forall x \in ℋ \|T (x)\| \leq {norm}_{ℎ} (y) {norm}_{ℎ} (x)) \to \exists z \in ℝ \forall x \in ℋ \|T (x)\| \leq z {norm}_{ℎ} (x)$
41	20 36 40	syl6an	$⊢ (T \in LinFn \land y \in ℋ) \to (\forall x \in ℋ T (x) = x \cdot_{ih} y \to \exists z \in ℝ \forall x \in ℋ \|T (x)\| \leq z {norm}_{ℎ} (x))$
42	41	rexlimdva	$⊢ T \in LinFn \to (\exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y \to \exists z \in ℝ \forall x \in ℋ \|T (x)\| \leq z {norm}_{ℎ} (x))$
43		lnfncon	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow \exists z \in ℝ \forall x \in ℋ \|T (x)\| \leq z {norm}_{ℎ} (x))$
44	42 43	sylibrd	$⊢ T \in LinFn \to (\exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y \to T \in ContFn)$
45	18 44	impbid	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y)$
46	1 45	bitr3d	$⊢ T \in LinFn \to ({norm}_{fn} (T) \in ℝ \leftrightarrow \exists y \in ℋ \forall x \in ℋ T (x) = x \cdot_{ih} y)$

Metamath Proof Explorer

Theorem riesz1

Proof