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 ⊢ T ∈ LinFn → norm fn ⁡ T ∈ ℝ ↔ ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y

Proof

Step Hyp Ref Expression
1 lnfncnbd ⊢ T ∈ LinFn → T ∈ ContFn ↔ norm fn ⁡ T ∈ ℝ
2 elin ⊢ T ∈ LinFn ∩ ContFn ↔ T ∈ LinFn ∧ T ∈ ContFn
3 fveq1 ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ x = if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ x
4 3 eqeq1d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ x = x ⋅ ih y ↔ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ x = x ⋅ ih y
5 4 rexralbidv ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y ↔ ∃ y ∈ ℋ ∀ x ∈ ℋ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ x = x ⋅ ih y
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 T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn
12 6 11 sselii ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn
13 inss2 ⊢ LinFn ∩ ContFn ⊆ ContFn
14 13 11 sselii ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
15 12 14 riesz3i ⊢ ∃ y ∈ ℋ ∀ x ∈ ℋ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ x = x ⋅ ih y
16 5 15 dedth ⊢ T ∈ LinFn ∩ ContFn → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
17 2 16 sylbir ⊢ T ∈ LinFn ∧ T ∈ ContFn → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
18 17 ex ⊢ T ∈ LinFn → T ∈ ContFn → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
19 normcl ⊢ y ∈ ℋ → norm ℎ ⁡ y ∈ ℝ
20 19 adantl ⊢ T ∈ LinFn ∧ y ∈ ℋ → norm ℎ ⁡ y ∈ ℝ
21 fveq2 ⊢ T ⁡ x = x ⋅ ih y → T ⁡ x = x ⋅ ih y
22 21 adantl ⊢ T ∈ LinFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ T ⁡ x = x ⋅ ih y → T ⁡ x = x ⋅ ih y
23 bcs ⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih y ≤ norm ℎ ⁡ x ⁢ norm ℎ ⁡ y
24 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
25 recn ⊢ norm ℎ ⁡ x ∈ ℝ → norm ℎ ⁡ x ∈ ℂ
26 recn ⊢ norm ℎ ⁡ y ∈ ℝ → norm ℎ ⁡ y ∈ ℂ
27 mulcom ⊢ norm ℎ ⁡ x ∈ ℂ ∧ norm ℎ ⁡ y ∈ ℂ → norm ℎ ⁡ x ⁢ norm ℎ ⁡ y = norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
28 25 26 27 syl2an ⊢ norm ℎ ⁡ x ∈ ℝ ∧ norm ℎ ⁡ y ∈ ℝ → norm ℎ ⁡ x ⁢ norm ℎ ⁡ y = norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
29 24 19 28 syl2an ⊢ x ∈ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ x ⁢ norm ℎ ⁡ y = norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
30 23 29 breqtrd ⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih y ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
31 30 adantll ⊢ T ∈ LinFn ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih y ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
32 31 adantr ⊢ T ∈ LinFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ T ⁡ x = x ⋅ ih y → x ⋅ ih y ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
33 22 32 eqbrtrd ⊢ T ∈ LinFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ T ⁡ x = x ⋅ ih y → T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
34 33 ex ⊢ T ∈ LinFn ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x = x ⋅ ih y → T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
35 34 an32s ⊢ T ∈ LinFn ∧ y ∈ ℋ ∧ x ∈ ℋ → T ⁡ x = x ⋅ ih y → T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
36 35 ralimdva ⊢ T ∈ LinFn ∧ y ∈ ℋ → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y → ∀ x ∈ ℋ T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
37 oveq1 ⊢ z = norm ℎ ⁡ y → z ⁢ norm ℎ ⁡ x = norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
38 37 breq2d ⊢ z = norm ℎ ⁡ y → T ⁡ x ≤ z ⁢ norm ℎ ⁡ x ↔ T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
39 38 ralbidv ⊢ z = norm ℎ ⁡ y → ∀ x ∈ ℋ T ⁡ x ≤ z ⁢ norm ℎ ⁡ x ↔ ∀ x ∈ ℋ T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x
40 39 rspcev ⊢ norm ℎ ⁡ y ∈ ℝ ∧ ∀ x ∈ ℋ T ⁡ x ≤ norm ℎ ⁡ y ⁢ norm ℎ ⁡ x → ∃ z ∈ ℝ ∀ x ∈ ℋ T ⁡ x ≤ z ⁢ norm ℎ ⁡ x
41 20 36 40 syl6an ⊢ T ∈ LinFn ∧ y ∈ ℋ → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y → ∃ z ∈ ℝ ∀ x ∈ ℋ T ⁡ x ≤ z ⁢ norm ℎ ⁡ x
42 41 rexlimdva ⊢ T ∈ LinFn → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y → ∃ z ∈ ℝ ∀ x ∈ ℋ T ⁡ x ≤ z ⁢ norm ℎ ⁡ x
43 lnfncon ⊢ T ∈ LinFn → T ∈ ContFn ↔ ∃ z ∈ ℝ ∀ x ∈ ℋ T ⁡ x ≤ z ⁢ norm ℎ ⁡ x
44 42 43 sylibrd ⊢ T ∈ LinFn → ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y → T ∈ ContFn
45 18 44 impbid ⊢ T ∈ LinFn → T ∈ ContFn ↔ ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
46 1 45 bitr3d ⊢ T ∈ LinFn → norm fn ⁡ T ∈ ℝ ↔ ∃ y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y