Theorem riesz1

Description: Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of Halmos p. 31. For part 2, see riesz2 . For the continuous linear functional version, see riesz3i and riesz4 . (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	riesz1	⊢ ( 𝑇 ∈ LinFn → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnfncnbd	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ( normfn ‘ 𝑇 ) ∈ ℝ ) )
2		elin	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) )
3		fveq1	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝑥 ) = ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) )
4	3	eqeq1d	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )
5	4	rexralbidv	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )
6		inss1	⊢ ( LinFn ∩ ContFn ) ⊆ LinFn
7		0lnfn	⊢ ( ℋ × { 0 } ) ∈ LinFn
8		0cnfn	⊢ ( ℋ × { 0 } ) ∈ ContFn
9		elin	⊢ ( ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) ↔ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( ℋ × { 0 } ) ∈ ContFn ) )
10	7 8 9	mpbir2an	⊢ ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn )
11	10	elimel	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn )
12	6 11	sselii	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
13		inss2	⊢ ( LinFn ∩ ContFn ) ⊆ ContFn
14	13 11	sselii	⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn
15	12 14	riesz3i	⊢ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 )
16	5 15	dedth	⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
17	2 16	sylbir	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
18	17	ex	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn → ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )
19		normcl	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
20	19	adantl	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ 𝑦 ) ∈ ℝ )
21		fveq2	⊢ ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) = ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) )
22	21	adantl	⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) = ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) )
23		bcs	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) )
24		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
25		recn	⊢ ( ( normℎ ‘ 𝑥 ) ∈ ℝ → ( normℎ ‘ 𝑥 ) ∈ ℂ )
26		recn	⊢ ( ( normℎ ‘ 𝑦 ) ∈ ℝ → ( normℎ ‘ 𝑦 ) ∈ ℂ )
27		mulcom	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( normℎ ‘ 𝑦 ) ∈ ℂ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
28	25 26 27	syl2an	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
29	24 19 28	syl2an	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ 𝑥 ) · ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
30	23 29	breqtrd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
31	30	adantll	⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
32	31	adantr	⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑥 ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
33	22 32	eqbrtrd	⊢ ( ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
34	33	ex	⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) )
35	34	an32s	⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) )
36	35	ralimdva	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) )
37		oveq1	⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( 𝑧 · ( normℎ ‘ 𝑥 ) ) = ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
38	37	breq2d	⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) )
39	38	ralbidv	⊢ ( 𝑧 = ( normℎ ‘ 𝑦 ) → ( ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) )
40	39	rspcev	⊢ ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) )
41	20 36 40	syl6an	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) )
42	41	rexlimdva	⊢ ( 𝑇 ∈ LinFn → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) )
43		lnfncon	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝑧 · ( normℎ ‘ 𝑥 ) ) ) )
44	42 43	sylibrd	⊢ ( 𝑇 ∈ LinFn → ( ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) → 𝑇 ∈ ContFn ) )
45	18 44	impbid	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )
46	1 45	bitr3d	⊢ ( 𝑇 ∈ LinFn → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )