Metamath Proof Explorer


Theorem rnbra

Description: The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion rnbra
|- ran bra = ( LinFn i^i ContFn )

Proof

Step Hyp Ref Expression
1 lnfncnbd
 |-  ( t e. LinFn -> ( t e. ContFn <-> ( normfn ` t ) e. RR ) )
2 1 pm5.32i
 |-  ( ( t e. LinFn /\ t e. ContFn ) <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) )
3 elin
 |-  ( t e. ( LinFn i^i ContFn ) <-> ( t e. LinFn /\ t e. ContFn ) )
4 ax-hilex
 |-  ~H e. _V
5 4 mptex
 |-  ( y e. ~H |-> ( y .ih x ) ) e. _V
6 df-bra
 |-  bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )
7 5 6 fnmpti
 |-  bra Fn ~H
8 fvelrnb
 |-  ( bra Fn ~H -> ( t e. ran bra <-> E. x e. ~H ( bra ` x ) = t ) )
9 7 8 ax-mp
 |-  ( t e. ran bra <-> E. x e. ~H ( bra ` x ) = t )
10 bralnfn
 |-  ( x e. ~H -> ( bra ` x ) e. LinFn )
11 brabn
 |-  ( x e. ~H -> ( normfn ` ( bra ` x ) ) e. RR )
12 10 11 jca
 |-  ( x e. ~H -> ( ( bra ` x ) e. LinFn /\ ( normfn ` ( bra ` x ) ) e. RR ) )
13 eleq1
 |-  ( ( bra ` x ) = t -> ( ( bra ` x ) e. LinFn <-> t e. LinFn ) )
14 fveq2
 |-  ( ( bra ` x ) = t -> ( normfn ` ( bra ` x ) ) = ( normfn ` t ) )
15 14 eleq1d
 |-  ( ( bra ` x ) = t -> ( ( normfn ` ( bra ` x ) ) e. RR <-> ( normfn ` t ) e. RR ) )
16 13 15 anbi12d
 |-  ( ( bra ` x ) = t -> ( ( ( bra ` x ) e. LinFn /\ ( normfn ` ( bra ` x ) ) e. RR ) <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) )
17 12 16 syl5ibcom
 |-  ( x e. ~H -> ( ( bra ` x ) = t -> ( t e. LinFn /\ ( normfn ` t ) e. RR ) ) )
18 17 rexlimiv
 |-  ( E. x e. ~H ( bra ` x ) = t -> ( t e. LinFn /\ ( normfn ` t ) e. RR ) )
19 riesz1
 |-  ( t e. LinFn -> ( ( normfn ` t ) e. RR <-> E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) ) )
20 19 biimpa
 |-  ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) )
21 braval
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( bra ` x ) ` y ) = ( y .ih x ) )
22 eqtr3
 |-  ( ( ( ( bra ` x ) ` y ) = ( y .ih x ) /\ ( t ` y ) = ( y .ih x ) ) -> ( ( bra ` x ) ` y ) = ( t ` y ) )
23 22 ex
 |-  ( ( ( bra ` x ) ` y ) = ( y .ih x ) -> ( ( t ` y ) = ( y .ih x ) -> ( ( bra ` x ) ` y ) = ( t ` y ) ) )
24 21 23 syl
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( t ` y ) = ( y .ih x ) -> ( ( bra ` x ) ` y ) = ( t ` y ) ) )
25 24 ralimdva
 |-  ( x e. ~H -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) )
26 25 adantl
 |-  ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) )
27 brafn
 |-  ( x e. ~H -> ( bra ` x ) : ~H --> CC )
28 lnfnf
 |-  ( t e. LinFn -> t : ~H --> CC )
29 28 adantr
 |-  ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> t : ~H --> CC )
30 ffn
 |-  ( ( bra ` x ) : ~H --> CC -> ( bra ` x ) Fn ~H )
31 ffn
 |-  ( t : ~H --> CC -> t Fn ~H )
32 eqfnfv
 |-  ( ( ( bra ` x ) Fn ~H /\ t Fn ~H ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) )
33 30 31 32 syl2an
 |-  ( ( ( bra ` x ) : ~H --> CC /\ t : ~H --> CC ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) )
34 27 29 33 syl2anr
 |-  ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( ( bra ` x ) = t <-> A. y e. ~H ( ( bra ` x ) ` y ) = ( t ` y ) ) )
35 26 34 sylibrd
 |-  ( ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) /\ x e. ~H ) -> ( A. y e. ~H ( t ` y ) = ( y .ih x ) -> ( bra ` x ) = t ) )
36 35 reximdva
 |-  ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> ( E. x e. ~H A. y e. ~H ( t ` y ) = ( y .ih x ) -> E. x e. ~H ( bra ` x ) = t ) )
37 20 36 mpd
 |-  ( ( t e. LinFn /\ ( normfn ` t ) e. RR ) -> E. x e. ~H ( bra ` x ) = t )
38 18 37 impbii
 |-  ( E. x e. ~H ( bra ` x ) = t <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) )
39 9 38 bitri
 |-  ( t e. ran bra <-> ( t e. LinFn /\ ( normfn ` t ) e. RR ) )
40 2 3 39 3bitr4ri
 |-  ( t e. ran bra <-> t e. ( LinFn i^i ContFn ) )
41 40 eqriv
 |-  ran bra = ( LinFn i^i ContFn )