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