Metamath Proof Explorer

Theorem riesz4

Description: A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of Beran p. 104. See riesz2 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion riesz4 ⊢ T ∈ LinFn ∩ ContFn → ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v = v ⋅ ih w

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ v = if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ v
2 1 eqeq1d ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → T ⁡ v = v ⋅ ih w ↔ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ v = v ⋅ ih w
3 2 ralbidv ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → ∀ v ∈ ℋ T ⁡ v = v ⋅ ih w ↔ ∀ v ∈ ℋ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ v = v ⋅ ih w
4 3 reubidv ⊢ T = if T ∈ LinFn ∩ ContFn T ℋ × 0 → ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v = v ⋅ ih w ↔ ∃! w ∈ ℋ ∀ v ∈ ℋ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ v = v ⋅ ih w
5 inss1 ⊢ LinFn ∩ ContFn ⊆ LinFn
6 0lnfn ⊢ ℋ × 0 ∈ LinFn
7 0cnfn ⊢ ℋ × 0 ∈ ContFn
8 elin ⊢ ℋ × 0 ∈ LinFn ∩ ContFn ↔ ℋ × 0 ∈ LinFn ∧ ℋ × 0 ∈ ContFn
9 6 7 8 mpbir2an ⊢ ℋ × 0 ∈ LinFn ∩ ContFn
10 9 elimel ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn ∩ ContFn
11 5 10 sselii ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ LinFn
12 inss2 ⊢ LinFn ∩ ContFn ⊆ ContFn
13 12 10 sselii ⊢ if T ∈ LinFn ∩ ContFn T ℋ × 0 ∈ ContFn
14 11 13 riesz4i ⊢ ∃! w ∈ ℋ ∀ v ∈ ℋ if T ∈ LinFn ∩ ContFn T ℋ × 0 ⁡ v = v ⋅ ih w
15 4 14 dedth ⊢ T ∈ LinFn ∩ ContFn → ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v = v ⋅ ih w