Theorem riesz4

Description: A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of Beran p. 104. See riesz2 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	riesz4	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists !w\in \mathscr{H}\forall v\in \mathscr{H}T\left(v\right)=v{\cdot }_{\mathrm{ih}}w$$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢T=if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\to T\left(v\right)=if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\left(v\right)$$
2	1	eqeq1d	$$⊢T=if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\to \left(T\left(v\right)=v{\cdot }_{\mathrm{ih}}w\leftrightarrow if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\left(v\right)=v{\cdot }_{\mathrm{ih}}w\right)$$
3	2	ralbidv	$$⊢T=if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\to \left(\forall v\in \mathscr{H}T\left(v\right)=v{\cdot }_{\mathrm{ih}}w\leftrightarrow \forall v\in \mathscr{H}if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\left(v\right)=v{\cdot }_{\mathrm{ih}}w\right)$$
4	3	reubidv	$$⊢T=if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\to \left(\exists !w\in \mathscr{H}\forall v\in \mathscr{H}T\left(v\right)=v{\cdot }_{\mathrm{ih}}w\leftrightarrow \exists !w\in \mathscr{H}\forall v\in \mathscr{H}if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\left(v\right)=v{\cdot }_{\mathrm{ih}}w\right)$$
5		inss1	$$⊢\mathrm{LinFn}\cap \mathrm{ContFn}\subseteq \mathrm{LinFn}$$
6		0lnfn	$$⊢\mathscr{H}\times \left\{0\right\}\in \mathrm{LinFn}$$
7		0cnfn	$$⊢\mathscr{H}\times \left\{0\right\}\in \mathrm{ContFn}$$
8		elin	$$⊢\mathscr{H}\times \left\{0\right\}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\leftrightarrow \left(\mathscr{H}\times \left\{0\right\}\in \mathrm{LinFn}\wedge \mathscr{H}\times \left\{0\right\}\in \mathrm{ContFn}\right)$$
9	6 7 8	mpbir2an	$$⊢\mathscr{H}\times \left\{0\right\}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$$
10	9	elimel	$$⊢if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$$
11	5 10	sselii	$$⊢if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{LinFn}$$
12		inss2	$$⊢\mathrm{LinFn}\cap \mathrm{ContFn}\subseteq \mathrm{ContFn}$$
13	12 10	sselii	$$⊢if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{ContFn}$$
14	11 13	riesz4i	$$⊢\exists !w\in \mathscr{H}\forall v\in \mathscr{H}if\left(T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right),T,\mathscr{H}\times \left\{0\right\}\right)\left(v\right)=v{\cdot }_{\mathrm{ih}}w$$
15	4 14	dedth	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists !w\in \mathscr{H}\forall v\in \mathscr{H}T\left(v\right)=v{\cdot }_{\mathrm{ih}}w$$