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

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

Proof of Theorem riesz4
StepHypRef Expression
1 fveq1 6102 . . . . 5 (𝑇 = if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) → (𝑇𝑣) = (if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0}))‘𝑣))
21eqeq1d 2612 . . . 4 (𝑇 = if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) → ((𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ (if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
32ralbidv 2969 . . 3 (𝑇 = if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) → (∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
43reubidv 3103 . 2 (𝑇 = if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) → (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤) ↔ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)))
5 inss1 3795 . . . 4 (LinFn ∩ ConFn) ⊆ LinFn
6 0lnfn 28228 . . . . . 6 ( ℋ × {0}) ∈ LinFn
7 0cnfn 28223 . . . . . 6 ( ℋ × {0}) ∈ ConFn
8 elin 3758 . . . . . 6 (( ℋ × {0}) ∈ (LinFn ∩ ConFn) ↔ (( ℋ × {0}) ∈ LinFn ∧ ( ℋ × {0}) ∈ ConFn))
96, 7, 8mpbir2an 957 . . . . 5 ( ℋ × {0}) ∈ (LinFn ∩ ConFn)
109elimel 4100 . . . 4 if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) ∈ (LinFn ∩ ConFn)
115, 10sselii 3565 . . 3 if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) ∈ LinFn
12 inss2 3796 . . . 4 (LinFn ∩ ConFn) ⊆ ConFn
1312, 10sselii 3565 . . 3 if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0})) ∈ ConFn
1411, 13riesz4i 28306 . 2 ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (if(𝑇 ∈ (LinFn ∩ ConFn), 𝑇, ( ℋ × {0}))‘𝑣) = (𝑣 ·ih 𝑤)
154, 14dedth 4089 1 (𝑇 ∈ (LinFn ∩ ConFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤))