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:1-1 ontoLinFnContFn

Proof

Step Hyp Ref Expression
1 ax-hilex V
2 1 mptex yyihxV
3 df-bra bra=xyyihx
4 2 3 fnmpti braFn
5 rnbra ranbra=LinFnContFn
6 fveq1 brax=braybraxz=brayz
7 braval xzbraxz=zihx
8 7 adantlr xyzbraxz=zihx
9 braval yzbrayz=zihy
10 9 adantll xyzbrayz=zihy
11 8 10 eqeq12d xyzbraxz=brayzzihx=zihy
12 6 11 syl5ib xyzbrax=brayzihx=zihy
13 12 ralrimdva xybrax=brayzzihx=zihy
14 hial2eq2 xyzzihx=zihyx=y
15 13 14 sylibd xybrax=brayx=y
16 15 rgen2 xybrax=brayx=y
17 dff1o6 bra:1-1 ontoLinFnContFnbraFnranbra=LinFnContFnxybrax=brayx=y
18 4 5 16 17 mpbir3an bra:1-1 ontoLinFnContFn