# Metamath Proof Explorer

## Theorem riesz4i

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

Ref Expression
Hypotheses nlelch.1 ${⊢}{T}\in \mathrm{LinFn}$
nlelch.2 ${⊢}{T}\in \mathrm{ContFn}$
Assertion riesz4i ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}$

### Proof

Step Hyp Ref Expression
1 nlelch.1 ${⊢}{T}\in \mathrm{LinFn}$
2 nlelch.2 ${⊢}{T}\in \mathrm{ContFn}$
3 1 2 riesz3i ${⊢}\exists {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}$
4 r19.26 ${⊢}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)↔\left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)$
5 oveq12 ${⊢}\left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to {T}\left({v}\right)-{T}\left({v}\right)=\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)$
6 5 adantl ${⊢}\left({v}\in ℋ\wedge \left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\right)\to {T}\left({v}\right)-{T}\left({v}\right)=\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)$
7 1 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
8 7 ffvelrni ${⊢}{v}\in ℋ\to {T}\left({v}\right)\in ℂ$
9 8 subidd ${⊢}{v}\in ℋ\to {T}\left({v}\right)-{T}\left({v}\right)=0$
10 9 adantr ${⊢}\left({v}\in ℋ\wedge \left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\right)\to {T}\left({v}\right)-{T}\left({v}\right)=0$
11 6 10 eqtr3d ${⊢}\left({v}\in ℋ\wedge \left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\right)\to \left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0$
12 11 ralimiaa ${⊢}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge {T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0$
13 4 12 sylbir ${⊢}\left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0$
14 hvsubcl ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to {w}{-}_{ℎ}{u}\in ℋ$
15 oveq1 ${⊢}{v}={w}{-}_{ℎ}{u}\to {v}{\cdot }_{\mathrm{ih}}{w}=\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}$
16 oveq1 ${⊢}{v}={w}{-}_{ℎ}{u}\to {v}{\cdot }_{\mathrm{ih}}{u}=\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}$
17 15 16 oveq12d ${⊢}{v}={w}{-}_{ℎ}{u}\to \left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)$
18 17 eqeq1d ${⊢}{v}={w}{-}_{ℎ}{u}\to \left(\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0↔\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)=0\right)$
19 18 rspcv ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0\to \left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)=0\right)$
20 14 19 syl ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0\to \left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)=0\right)$
21 normcl ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to {norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)\in ℝ$
22 21 recnd ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to {norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)\in ℂ$
23 sqeq0 ${⊢}{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)\in ℂ\to \left({{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=0↔{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)=0\right)$
24 22 23 syl ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to \left({{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=0↔{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)=0\right)$
25 norm-i ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)=0↔{w}{-}_{ℎ}{u}={0}_{ℎ}\right)$
26 24 25 bitrd ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to \left({{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=0↔{w}{-}_{ℎ}{u}={0}_{ℎ}\right)$
27 14 26 syl ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left({{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=0↔{w}{-}_{ℎ}{u}={0}_{ℎ}\right)$
28 normsq ${⊢}{w}{-}_{ℎ}{u}\in ℋ\to {{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}\left({w}{-}_{ℎ}{u}\right)$
29 14 28 syl ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to {{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}\left({w}{-}_{ℎ}{u}\right)$
30 simpl ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to {w}\in ℋ$
31 simpr ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to {u}\in ℋ$
32 his2sub2 ${⊢}\left({w}{-}_{ℎ}{u}\in ℋ\wedge {w}\in ℋ\wedge {u}\in ℋ\right)\to \left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}\left({w}{-}_{ℎ}{u}\right)=\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)$
33 14 30 31 32 syl3anc ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}\left({w}{-}_{ℎ}{u}\right)=\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)$
34 29 33 eqtrd ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to {{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)$
35 34 eqeq1d ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left({{norm}_{ℎ}\left({w}{-}_{ℎ}{u}\right)}^{2}=0↔\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)=0\right)$
36 hvsubeq0 ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left({w}{-}_{ℎ}{u}={0}_{ℎ}↔{w}={u}\right)$
37 27 35 36 3bitr3d ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left(\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{w}\right)-\left(\left({w}{-}_{ℎ}{u}\right){\cdot }_{\mathrm{ih}}{u}\right)=0↔{w}={u}\right)$
38 20 37 sylibd ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}\left({v}{\cdot }_{\mathrm{ih}}{w}\right)-\left({v}{\cdot }_{\mathrm{ih}}{u}\right)=0\to {w}={u}\right)$
39 13 38 syl5 ${⊢}\left({w}\in ℋ\wedge {u}\in ℋ\right)\to \left(\left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to {w}={u}\right)$
40 39 rgen2 ${⊢}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {u}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to {w}={u}\right)$
41 oveq2 ${⊢}{w}={u}\to {v}{\cdot }_{\mathrm{ih}}{w}={v}{\cdot }_{\mathrm{ih}}{u}$
42 41 eqeq2d ${⊢}{w}={u}\to \left({T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)$
43 42 ralbidv ${⊢}{w}={u}\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)$
44 43 reu4 ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔\left(\exists {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {u}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}\wedge \forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{u}\right)\to {w}={u}\right)\right)$
45 3 40 44 mpbir2an ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}$