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	ffvelrni	⊢ ( 𝑣 ∈ ℋ → ( 𝑇 ‘ 𝑣 ) ∈ ℂ )
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 𝑤 )