Fundamental theorem of Hilbert spaces

In mathematics, specifically in functional analysis and Hilbert space theory, the Fundamental Theorem of Hilbert spaces gives a necessarily and sufficient condition for a Hausdorff pre-Hilbert space to be a Hilbert space in terms of the canonical isometry of a pre-Hilbert space into its anti-dual. 
Preliminaries.
Antilinear functionals and the anti-dual.
Suppose that is a topological vector space (TVS). 
A function is called semilinear or antilinear if for all and all scalars ,
The vector space of all continuous antilinear functions on is called the anti-dual space or complex conjugate dual space of and is denoted by formula_1 (in contrast, the continuous dual space of is denoted by formula_2), which we make into a normed space by endowing it with the canonical norm (defined in the same way as the canonical norm on the continuous dual space of ). 
Pre-Hilbert spaces and sesquilinear forms.
A sesquilinear form is a map such that for all , the map defined by is linear, and for all , the map defined by is antilinear. 
Note that in Physics, the convention is that a sesquilinear form is linear in its "second" coordinate and antilinear in its first coordinate. 
A sesquilinear form on is called positive definite if for all non-0 ; it is called non-negative if for all . 
A sesquilinear form on is called a Hermitian form if in addition it has the property that formula_3 for all .
Pre-Hilbert and Hilbert spaces.
A pre-Hilbert space is a pair consisting of a vector space and a non-negative sesquilinear form on ; 
if in addition this sesquilinear form is positive definite then is called a Hausdorff pre-Hilbert space. 
If is non-negative then it induces a canonical seminorm on , denoted by formula_4, defined by , where if is also positive definite then this map is a norm. 
This canonical semi-norm makes every pre-Hilbert space into a seminormed space and every Hausdorff pre-Hilbert space into a normed space. 
The sesquilinear form is separately uniformly continuous in each of its two arguments and hence can be extended to a separately continuous sesquilinear form on the completion of ; if is Hausdorff then this completion is a Hilbert space. 
A Hausdorff pre-Hilbert space that is complete is called a Hilbert space.
Canonical map into the anti-dual.
Suppose is a pre-Hilbert space. If , we define the canonical maps:
The canonical map from into its anti-dual formula_1 is the map 
If is a pre-Hilbert space then this canonical map is linear and continuous; 
this map is an isometry onto a vector subspace of the anti-dual if and only if is a Hausdorff pre-Hilbert. 
There is of course a canonical antilinear surjective isometry formula_7 that sends a continuous linear functional on to the continuous antilinear functional denoted by and defined by .