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 )