This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 ∈ LinFn
nlelch.2 ⊢ 𝑇 ∈ ContFn
Assertion riesz4i ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 )

Proof

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