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 ⋅ ih w

Proof

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