Metamath Proof Explorer


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 𝑦 ) ) )