Metamath Proof Explorer

Theorem bra11

Description: The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion bra11 
|- bra : ~H -1-1-onto-> ( LinFn i^i ContFn )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 mptex 
 |-  ( y e. ~H |-> ( y .ih x ) ) e. _V
3 df-bra 
 |-  bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )
4 2 3 fnmpti 
 |-  bra Fn ~H
5 rnbra 
 |-  ran bra = ( LinFn i^i ContFn )
6 fveq1 
 |-  ( ( bra ` x ) = ( bra ` y ) -> ( ( bra ` x ) ` z ) = ( ( bra ` y ) ` z ) )
7 braval 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( bra ` x ) ` z ) = ( z .ih x ) )
8 7 adantlr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( bra ` x ) ` z ) = ( z .ih x ) )
9 braval 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( bra ` y ) ` z ) = ( z .ih y ) )
10 9 adantll 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( bra ` y ) ` z ) = ( z .ih y ) )
11 8 10 eqeq12d 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( ( bra ` x ) ` z ) = ( ( bra ` y ) ` z ) <-> ( z .ih x ) = ( z .ih y ) ) )
12 6 11 imbitrid 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( bra ` x ) = ( bra ` y ) -> ( z .ih x ) = ( z .ih y ) ) )
13 12 ralrimdva 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( bra ` x ) = ( bra ` y ) -> A. z e. ~H ( z .ih x ) = ( z .ih y ) ) )
14 hial2eq2 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( A. z e. ~H ( z .ih x ) = ( z .ih y ) <-> x = y ) )
15 13 14 sylibd 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( bra ` x ) = ( bra ` y ) -> x = y ) )
16 15 rgen2 
 |-  A. x e. ~H A. y e. ~H ( ( bra ` x ) = ( bra ` y ) -> x = y )
17 dff1o6 
 |-  ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) <-> ( bra Fn ~H /\ ran bra = ( LinFn i^i ContFn ) /\ A. x e. ~H A. y e. ~H ( ( bra ` x ) = ( bra ` y ) -> x = y ) ) )
18 4 5 16 17 mpbir3an 
 |-  bra : ~H -1-1-onto-> ( LinFn i^i ContFn )