Metamath Proof Explorer

Theorem riesz4i

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

Ref Expression
Hypotheses nlelch.1 
|- T e. LinFn
nlelch.2 
|- T e. ContFn
Assertion riesz4i 
|- E! w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )

Proof

Step Hyp Ref Expression
1 nlelch.1 
 |-  T e. LinFn
2 nlelch.2 
 |-  T e. ContFn
3 1 2 riesz3i 
 |-  E. w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )
4 r19.26 
 |-  ( A. v e. ~H ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) <-> ( A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. v e. ~H ( T ` v ) = ( v .ih u ) ) )
5 oveq12 
 |-  ( ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) -> ( ( T ` v ) - ( T ` v ) ) = ( ( v .ih w ) - ( v .ih u ) ) )
6 5 adantl 
 |-  ( ( v e. ~H /\ ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) ) -> ( ( T ` v ) - ( T ` v ) ) = ( ( v .ih w ) - ( v .ih u ) ) )
7 1 lnfnfi 
 |-  T : ~H --> CC
8 7 ffvelcdmi 
 |-  ( v e. ~H -> ( T ` v ) e. CC )
9 8 subidd 
 |-  ( v e. ~H -> ( ( T ` v ) - ( T ` v ) ) = 0 )
10 9 adantr 
 |-  ( ( v e. ~H /\ ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) ) -> ( ( T ` v ) - ( T ` v ) ) = 0 )
11 6 10 eqtr3d 
 |-  ( ( v e. ~H /\ ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) ) -> ( ( v .ih w ) - ( v .ih u ) ) = 0 )
12 11 ralimiaa 
 |-  ( A. v e. ~H ( ( T ` v ) = ( v .ih w ) /\ ( T ` v ) = ( v .ih u ) ) -> A. v e. ~H ( ( v .ih w ) - ( v .ih u ) ) = 0 )
13 4 12 sylbir 
 |-  ( ( A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. v e. ~H ( T ` v ) = ( v .ih u ) ) -> A. v e. ~H ( ( v .ih w ) - ( v .ih u ) ) = 0 )
14 hvsubcl 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( w -h u ) e. ~H )
15 oveq1 
 |-  ( v = ( w -h u ) -> ( v .ih w ) = ( ( w -h u ) .ih w ) )
16 oveq1 
 |-  ( v = ( w -h u ) -> ( v .ih u ) = ( ( w -h u ) .ih u ) )
17 15 16 oveq12d 
 |-  ( v = ( w -h u ) -> ( ( v .ih w ) - ( v .ih u ) ) = ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) )
18 17 eqeq1d 
 |-  ( v = ( w -h u ) -> ( ( ( v .ih w ) - ( v .ih u ) ) = 0 <-> ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) = 0 ) )
19 18 rspcv 
 |-  ( ( w -h u ) e. ~H -> ( A. v e. ~H ( ( v .ih w ) - ( v .ih u ) ) = 0 -> ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) = 0 ) )
20 14 19 syl 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( A. v e. ~H ( ( v .ih w ) - ( v .ih u ) ) = 0 -> ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) = 0 ) )
21 normcl 
 |-  ( ( w -h u ) e. ~H -> ( normh ` ( w -h u ) ) e. RR )
22 21 recnd 
 |-  ( ( w -h u ) e. ~H -> ( normh ` ( w -h u ) ) e. CC )
23 sqeq0 
 |-  ( ( normh ` ( w -h u ) ) e. CC -> ( ( ( normh ` ( w -h u ) ) ^ 2 ) = 0 <-> ( normh ` ( w -h u ) ) = 0 ) )
24 22 23 syl 
 |-  ( ( w -h u ) e. ~H -> ( ( ( normh ` ( w -h u ) ) ^ 2 ) = 0 <-> ( normh ` ( w -h u ) ) = 0 ) )
25 norm-i 
 |-  ( ( w -h u ) e. ~H -> ( ( normh ` ( w -h u ) ) = 0 <-> ( w -h u ) = 0h ) )
26 24 25 bitrd 
 |-  ( ( w -h u ) e. ~H -> ( ( ( normh ` ( w -h u ) ) ^ 2 ) = 0 <-> ( w -h u ) = 0h ) )
27 14 26 syl 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( ( normh ` ( w -h u ) ) ^ 2 ) = 0 <-> ( w -h u ) = 0h ) )
28 normsq 
 |-  ( ( w -h u ) e. ~H -> ( ( normh ` ( w -h u ) ) ^ 2 ) = ( ( w -h u ) .ih ( w -h u ) ) )
29 14 28 syl 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( normh ` ( w -h u ) ) ^ 2 ) = ( ( w -h u ) .ih ( w -h u ) ) )
30 simpl 
 |-  ( ( w e. ~H /\ u e. ~H ) -> w e. ~H )
31 simpr 
 |-  ( ( w e. ~H /\ u e. ~H ) -> u e. ~H )
32 his2sub2 
 |-  ( ( ( w -h u ) e. ~H /\ w e. ~H /\ u e. ~H ) -> ( ( w -h u ) .ih ( w -h u ) ) = ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) )
33 14 30 31 32 syl3anc 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( w -h u ) .ih ( w -h u ) ) = ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) )
34 29 33 eqtrd 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( normh ` ( w -h u ) ) ^ 2 ) = ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) )
35 34 eqeq1d 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( ( normh ` ( w -h u ) ) ^ 2 ) = 0 <-> ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) = 0 ) )
36 hvsubeq0 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( w -h u ) = 0h <-> w = u ) )
37 27 35 36 3bitr3d 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( ( ( w -h u ) .ih w ) - ( ( w -h u ) .ih u ) ) = 0 <-> w = u ) )
38 20 37 sylibd 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( A. v e. ~H ( ( v .ih w ) - ( v .ih u ) ) = 0 -> w = u ) )
39 13 38 syl5 
 |-  ( ( w e. ~H /\ u e. ~H ) -> ( ( A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. v e. ~H ( T ` v ) = ( v .ih u ) ) -> w = u ) )
40 39 rgen2 
 |-  A. w e. ~H A. u e. ~H ( ( A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. v e. ~H ( T ` v ) = ( v .ih u ) ) -> w = u )
41 oveq2 
 |-  ( w = u -> ( v .ih w ) = ( v .ih u ) )
42 41 eqeq2d 
 |-  ( w = u -> ( ( T ` v ) = ( v .ih w ) <-> ( T ` v ) = ( v .ih u ) ) )
43 42 ralbidv 
 |-  ( w = u -> ( A. v e. ~H ( T ` v ) = ( v .ih w ) <-> A. v e. ~H ( T ` v ) = ( v .ih u ) ) )
44 43 reu4 
 |-  ( E! w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w ) <-> ( E. w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. w e. ~H A. u e. ~H ( ( A. v e. ~H ( T ` v ) = ( v .ih w ) /\ A. v e. ~H ( T ` v ) = ( v .ih u ) ) -> w = u ) ) )
45 3 40 44 mpbir2an 
 |-  E! w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )