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∈LinFn
nlelch.2 ⊢T∈ContFn
Assertion riesz4i ⊢∃!w∈ℋ∀v∈ℋT⁡v=v⋅ihw

Proof

Step Hyp Ref Expression
1 nlelch.1 ⊢T∈LinFn
2 nlelch.2 ⊢T∈ContFn
3 1 2 riesz3i ⊢∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw
4 r19.26 ⊢∀v∈ℋT⁡v=v⋅ihw∧T⁡v=v⋅ihu↔∀v∈ℋT⁡v=v⋅ihw∧∀v∈ℋT⁡v=v⋅ihu
5 oveq12 ⊢T⁡v=v⋅ihw∧T⁡v=v⋅ihu→T⁡v−T⁡v=v⋅ihw−v⋅ihu
6 5 adantl ⊢v∈ℋ∧T⁡v=v⋅ihw∧T⁡v=v⋅ihu→T⁡v−T⁡v=v⋅ihw−v⋅ihu
7 1 lnfnfi ⊢T:ℋ⟶ℂ
8 7 ffvelcdmi ⊢v∈ℋ→T⁡v∈ℂ
9 8 subidd ⊢v∈ℋ→T⁡v−T⁡v=0
10 9 adantr ⊢v∈ℋ∧T⁡v=v⋅ihw∧T⁡v=v⋅ihu→T⁡v−T⁡v=0
11 6 10 eqtr3d ⊢v∈ℋ∧T⁡v=v⋅ihw∧T⁡v=v⋅ihu→v⋅ihw−v⋅ihu=0
12 11 ralimiaa ⊢∀v∈ℋT⁡v=v⋅ihw∧T⁡v=v⋅ihu→∀v∈ℋv⋅ihw−v⋅ihu=0
13 4 12 sylbir ⊢∀v∈ℋT⁡v=v⋅ihw∧∀v∈ℋT⁡v=v⋅ihu→∀v∈ℋv⋅ihw−v⋅ihu=0
14 hvsubcl ⊢w∈ℋ∧u∈ℋ→w-ℎu∈ℋ
15 oveq1 ⊢v=w-ℎu→v⋅ihw=w-ℎu⋅ihw
16 oveq1 ⊢v=w-ℎu→v⋅ihu=w-ℎu⋅ihu
17 15 16 oveq12d ⊢v=w-ℎu→v⋅ihw−v⋅ihu=w-ℎu⋅ihw−w-ℎu⋅ihu
18 17 eqeq1d ⊢v=w-ℎu→v⋅ihw−v⋅ihu=0↔w-ℎu⋅ihw−w-ℎu⋅ihu=0
19 18 rspcv ⊢w-ℎu∈ℋ→∀v∈ℋv⋅ihw−v⋅ihu=0→w-ℎu⋅ihw−w-ℎu⋅ihu=0
20 14 19 syl ⊢w∈ℋ∧u∈ℋ→∀v∈ℋv⋅ihw−v⋅ihu=0→w-ℎu⋅ihw−w-ℎu⋅ihu=0
21 normcl ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu∈ℝ
22 21 recnd ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu∈ℂ
23 sqeq0 ⊢normℎ⁡w-ℎu∈ℂ→normℎ⁡w-ℎu2=0↔normℎ⁡w-ℎu=0
24 22 23 syl ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu2=0↔normℎ⁡w-ℎu=0
25 norm-i ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu=0↔w-ℎu=0ℎ
26 24 25 bitrd ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu2=0↔w-ℎu=0ℎ
27 14 26 syl ⊢w∈ℋ∧u∈ℋ→normℎ⁡w-ℎu2=0↔w-ℎu=0ℎ
28 normsq ⊢w-ℎu∈ℋ→normℎ⁡w-ℎu2=w-ℎu⋅ihw-ℎu
29 14 28 syl ⊢w∈ℋ∧u∈ℋ→normℎ⁡w-ℎu2=w-ℎu⋅ihw-ℎu
30 simpl ⊢w∈ℋ∧u∈ℋ→w∈ℋ
31 simpr ⊢w∈ℋ∧u∈ℋ→u∈ℋ
32 his2sub2 ⊢w-ℎu∈ℋ∧w∈ℋ∧u∈ℋ→w-ℎu⋅ihw-ℎu=w-ℎu⋅ihw−w-ℎu⋅ihu
33 14 30 31 32 syl3anc ⊢w∈ℋ∧u∈ℋ→w-ℎu⋅ihw-ℎu=w-ℎu⋅ihw−w-ℎu⋅ihu
34 29 33 eqtrd ⊢w∈ℋ∧u∈ℋ→normℎ⁡w-ℎu2=w-ℎu⋅ihw−w-ℎu⋅ihu
35 34 eqeq1d ⊢w∈ℋ∧u∈ℋ→normℎ⁡w-ℎu2=0↔w-ℎu⋅ihw−w-ℎu⋅ihu=0
36 hvsubeq0 ⊢w∈ℋ∧u∈ℋ→w-ℎu=0ℎ↔w=u
37 27 35 36 3bitr3d ⊢w∈ℋ∧u∈ℋ→w-ℎu⋅ihw−w-ℎu⋅ihu=0↔w=u
38 20 37 sylibd ⊢w∈ℋ∧u∈ℋ→∀v∈ℋv⋅ihw−v⋅ihu=0→w=u
39 13 38 syl5 ⊢w∈ℋ∧u∈ℋ→∀v∈ℋT⁡v=v⋅ihw∧∀v∈ℋT⁡v=v⋅ihu→w=u
40 39 rgen2 ⊢∀w∈ℋ∀u∈ℋ∀v∈ℋT⁡v=v⋅ihw∧∀v∈ℋT⁡v=v⋅ihu→w=u
41 oveq2 ⊢w=u→v⋅ihw=v⋅ihu
42 41 eqeq2d ⊢w=u→T⁡v=v⋅ihw↔T⁡v=v⋅ihu
43 42 ralbidv ⊢w=u→∀v∈ℋT⁡v=v⋅ihw↔∀v∈ℋT⁡v=v⋅ihu
44 43 reu4 ⊢∃!w∈ℋ∀v∈ℋT⁡v=v⋅ihw↔∃w∈ℋ∀v∈ℋT⁡v=v⋅ihw∧∀w∈ℋ∀u∈ℋ∀v∈ℋT⁡v=v⋅ihw∧∀v∈ℋT⁡v=v⋅ihu→w=u
45 3 40 44 mpbir2an ⊢∃!w∈ℋ∀v∈ℋT⁡v=v⋅ihw