Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  riesz4 Structured version   Visualization version   GIF version

Theorem riesz4 28893
 Description: A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 28895 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
riesz4 (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤))
Distinct variable group:   𝑤,𝑣,𝑇

Proof of Theorem riesz4
StepHypRef Expression
1 fveq1 6177 . . . . 5 (𝑇 = if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) → (𝑇𝑣) = (if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0}))‘𝑣))
21eqeq1d 2622 . . . 4 (𝑇 = if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) → ((𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ (if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
32ralbidv 2983 . . 3 (𝑇 = if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) → (∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
43reubidv 3121 . 2 (𝑇 = if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) → (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
5 inss1 3825 . . . 4 (LinFn ∩ ContFn) ⊆ LinFn
6 0lnfn 28814 . . . . . 6 ( ℋ × {0}) ∈ LinFn
7 0cnfn 28809 . . . . . 6 ( ℋ × {0}) ∈ ContFn
8 elin 3788 . . . . . 6 (( ℋ × {0}) ∈ (LinFn ∩ ContFn) ↔ (( ℋ × {0}) ∈ LinFn ∧ ( ℋ × {0}) ∈ ContFn))
96, 7, 8mpbir2an 954 . . . . 5 ( ℋ × {0}) ∈ (LinFn ∩ ContFn)
109elimel 4141 . . . 4 if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) ∈ (LinFn ∩ ContFn)
115, 10sselii 3592 . . 3 if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) ∈ LinFn
12 inss2 3826 . . . 4 (LinFn ∩ ContFn) ⊆ ContFn
1312, 10sselii 3592 . . 3 if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0})) ∈ ContFn
1411, 13riesz4i 28892 . 2 ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ContFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)
154, 14dedth 4130 1 (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤))