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 ffvelrni
 |-  ( 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 )