This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑤 ) )