Metamath Proof Explorer

Theorem riesz1

Description: Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of Halmos p. 31. For part 2, see riesz2 . For the continuous linear functional version, see riesz3i and riesz4 . (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion riesz1 
|- ( T e. LinFn -> ( ( normfn ` T ) e. RR <-> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )

Proof

Step Hyp Ref Expression
1 lnfncnbd 
 |-  ( T e. LinFn -> ( T e. ContFn <-> ( normfn ` T ) e. RR ) )
2 elin 
 |-  ( T e. ( LinFn i^i ContFn ) <-> ( T e. LinFn /\ T e. ContFn ) )
3 fveq1 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( T ` x ) = ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` x ) )
4 3 eqeq1d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( ( T ` x ) = ( x .ih y ) <-> ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` x ) = ( x .ih y ) ) )
5 4 rexralbidv 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) <-> E. y e. ~H A. x e. ~H ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` x ) = ( x .ih y ) ) )
6 inss1 
 |-  ( LinFn i^i ContFn ) C_ LinFn
7 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
8 0cnfn 
 |-  ( ~H X. { 0 } ) e. ContFn
9 elin 
 |-  ( ( ~H X. { 0 } ) e. ( LinFn i^i ContFn ) <-> ( ( ~H X. { 0 } ) e. LinFn /\ ( ~H X. { 0 } ) e. ContFn ) )
10 7 8 9 mpbir2an 
 |-  ( ~H X. { 0 } ) e. ( LinFn i^i ContFn )
11 10 elimel 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ( LinFn i^i ContFn )
12 6 11 sselii 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. LinFn
13 inss2 
 |-  ( LinFn i^i ContFn ) C_ ContFn
14 13 11 sselii 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ContFn
15 12 14 riesz3i 
 |-  E. y e. ~H A. x e. ~H ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` x ) = ( x .ih y )
16 5 15 dedth 
 |-  ( T e. ( LinFn i^i ContFn ) -> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )
17 2 16 sylbir 
 |-  ( ( T e. LinFn /\ T e. ContFn ) -> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )
18 17 ex 
 |-  ( T e. LinFn -> ( T e. ContFn -> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )
19 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
20 19 adantl 
 |-  ( ( T e. LinFn /\ y e. ~H ) -> ( normh ` y ) e. RR )
21 fveq2 
 |-  ( ( T ` x ) = ( x .ih y ) -> ( abs ` ( T ` x ) ) = ( abs ` ( x .ih y ) ) )
22 21 adantl 
 |-  ( ( ( ( T e. LinFn /\ x e. ~H ) /\ y e. ~H ) /\ ( T ` x ) = ( x .ih y ) ) -> ( abs ` ( T ` x ) ) = ( abs ` ( x .ih y ) ) )
23 bcs 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( abs ` ( x .ih y ) ) <_ ( ( normh ` x ) x. ( normh ` y ) ) )
24 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
25 recn 
 |-  ( ( normh ` x ) e. RR -> ( normh ` x ) e. CC )
26 recn 
 |-  ( ( normh ` y ) e. RR -> ( normh ` y ) e. CC )
27 mulcom 
 |-  ( ( ( normh ` x ) e. CC /\ ( normh ` y ) e. CC ) -> ( ( normh ` x ) x. ( normh ` y ) ) = ( ( normh ` y ) x. ( normh ` x ) ) )
28 25 26 27 syl2an 
 |-  ( ( ( normh ` x ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normh ` x ) x. ( normh ` y ) ) = ( ( normh ` y ) x. ( normh ` x ) ) )
29 24 19 28 syl2an 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( normh ` x ) x. ( normh ` y ) ) = ( ( normh ` y ) x. ( normh ` x ) ) )
30 23 29 breqtrd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( abs ` ( x .ih y ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) )
31 30 adantll 
 |-  ( ( ( T e. LinFn /\ x e. ~H ) /\ y e. ~H ) -> ( abs ` ( x .ih y ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) )
32 31 adantr 
 |-  ( ( ( ( T e. LinFn /\ x e. ~H ) /\ y e. ~H ) /\ ( T ` x ) = ( x .ih y ) ) -> ( abs ` ( x .ih y ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) )
33 22 32 eqbrtrd 
 |-  ( ( ( ( T e. LinFn /\ x e. ~H ) /\ y e. ~H ) /\ ( T ` x ) = ( x .ih y ) ) -> ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) )
34 33 ex 
 |-  ( ( ( T e. LinFn /\ x e. ~H ) /\ y e. ~H ) -> ( ( T ` x ) = ( x .ih y ) -> ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) )
35 34 an32s 
 |-  ( ( ( T e. LinFn /\ y e. ~H ) /\ x e. ~H ) -> ( ( T ` x ) = ( x .ih y ) -> ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) )
36 35 ralimdva 
 |-  ( ( T e. LinFn /\ y e. ~H ) -> ( A. x e. ~H ( T ` x ) = ( x .ih y ) -> A. x e. ~H ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) )
37 oveq1 
 |-  ( z = ( normh ` y ) -> ( z x. ( normh ` x ) ) = ( ( normh ` y ) x. ( normh ` x ) ) )
38 37 breq2d 
 |-  ( z = ( normh ` y ) -> ( ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) <-> ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) )
39 38 ralbidv 
 |-  ( z = ( normh ` y ) -> ( A. x e. ~H ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) <-> A. x e. ~H ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) )
40 39 rspcev 
 |-  ( ( ( normh ` y ) e. RR /\ A. x e. ~H ( abs ` ( T ` x ) ) <_ ( ( normh ` y ) x. ( normh ` x ) ) ) -> E. z e. RR A. x e. ~H ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) )
41 20 36 40 syl6an 
 |-  ( ( T e. LinFn /\ y e. ~H ) -> ( A. x e. ~H ( T ` x ) = ( x .ih y ) -> E. z e. RR A. x e. ~H ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) ) )
42 41 rexlimdva 
 |-  ( T e. LinFn -> ( E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) -> E. z e. RR A. x e. ~H ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) ) )
43 lnfncon 
 |-  ( T e. LinFn -> ( T e. ContFn <-> E. z e. RR A. x e. ~H ( abs ` ( T ` x ) ) <_ ( z x. ( normh ` x ) ) ) )
44 42 43 sylibrd 
 |-  ( T e. LinFn -> ( E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) -> T e. ContFn ) )
45 18 44 impbid 
 |-  ( T e. LinFn -> ( T e. ContFn <-> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )
46 1 45 bitr3d 
 |-  ( T e. LinFn -> ( ( normfn ` T ) e. RR <-> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )