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 ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )

Proof

Step Hyp Ref Expression
1 fveq1 ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇𝑣 ) = ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) )
2 1 eqeq1d ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) )
3 2 ralbidv ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) )
4 3 reubidv ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) )
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 ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn )
11 5 10 sselii if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
12 inss2 ( LinFn ∩ ContFn ) ⊆ ContFn
13 12 10 sselii if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn
14 11 13 riesz4i ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 )
15 4 14 dedth ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )