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