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

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