avewright/proofwiki-math huggingface dataset:
Theorem: Real Part of Linear Functional is Linear Functional

Let $X$ be a vector space over $\C$. 
Let $f : X \to \C$ be a linear functional. 
Define $g : X \to \R$ by: 
:$\map g x = \map \Re {\map f x}$
for each $x \in X$.
Then $f$ is $\R$-linear.

Proof:
Let $x, y \in X$ and $\lambda, \mu \in \R$. 
Then:
{{begin-eqn}}
{{eqn	| l = \map g {\lambda x + \mu y}
		| r = \map \Re {\map f {\lambda x + \mu y} }
}}
{{eqn	| r = \frac 1 2 \paren {\map f {\lambda x + \mu y} + \overline {\map f {\lambda x + \mu y} } }
		| c = Sum of Complex Number with Conjugate
}}
{{eqn	| r = \frac 1 2 \paren {\lambda \map f x + \mu \map f y + \overline {\lambda \map f x} + \overline {\mu \map f y} }
		| c = Sum of Complex Conjugates, linearity of $f$
}}
{{eqn	| r = \frac 1 2 \paren {\lambda \map f x + \mu \map f y + \lambda \overline {\map f x} + \mu \overline {\map f y} }
		| c = Product of Complex Conjugates
}}
{{eqn	| r = \frac \lambda 2 \paren {\map f x + \overline {\map f x} } + \frac \mu 2 \paren {\map f y + \overline {\map f y} }
}}
{{eqn	| r = \lambda \map g x + \mu \map g y
}}
{{end-eqn}}
{{qed}}
Category:Linear Functionals
tt7xlo4g480uziozh8yi4e9vsygh99e
Theorem: Imaginary Part of Linear Functional is Linear Functional

Let $X$ be a vector space over $\C$. 
Let $f : X \to \C$ be a linear functional. 
Define $h : X \to \R$ by: 
:$\map h x = \map \Im {\map f x}$
for each $x \in X$.
Then $f$ is $\R$-linear.

Proof:
Let $x, y \in X$ and $\lambda, \mu \in \R$. 
Then:
{{begin-eqn}}
{{eqn	| l = \map h {\lambda x + \mu y}
		| r = \map \Re {\map f {\lambda x + \mu y} }
}}
{{eqn	| r = \frac 1 {2 i} \paren {\map f {\lambda x + \mu y} - \overline {\map f {\lambda x + \mu y} } }
		| c = Difference of Complex Number with Conjugate
}}
{{eqn	| r = \frac 1 {2 i} \paren {\lambda \map f x + \mu \map f y - \overline {\lambda \map f x} - \overline {\mu \map f y} }
		| c = Sum of Complex Conjugates, linearity of $f$
}}
{{eqn	| r = \frac 1 {2 i} \paren {\lambda \map f x + \mu \map f y - \lambda \overline {\map f x} - \mu \overline {\map f y} }
		| c = Product of Complex Conjugates
}}
{{eqn	| r = \frac \lambda {2 i} \paren {\map f x - \overline {\map f x} } + \frac \mu {2 i} \paren {\map f y - \overline {\map f y} }
}}
{{eqn	| r = \lambda \map g x + \mu \map g y
}}
{{end-eqn}}
{{qed}}
Category:Linear Functionals
r0c0y3zo5orkpumeq6xix4s35ft8an8
Theorem: Hahn-Banach Theorem for Continuous Linear Functional on Locally Convex Space

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \PP}$ be a locally convex space over $\GF$ with its standard topology.
Let $X_0$ be a linear subspace of $X$. 
Let $f_0 : X_0 \to \GF$ be a continuous linear functional.
Then there exists a continuous linear functional $f : X \to \GF$ such that $f$ extends $f_0$.

Proof:
By Normed Vector Space is Locally Convex Space and Norm on Vector Space is Seminorm, we can view the normed vector space $\struct {\GF, \cmod {\, \cdot \,} }$ as the locally convex space $\struct {\GF, \set {\cmod {\, \cdot \,} } }$.
From Characterization of Continuous Linear Transformations between Locally Convex Spaces, there exists $C > 0$, $n \in \N$ and $p_1, \ldots, p_n \in \PP$ such that: 
:$\ds \cmod {\map {f_0} x} \le C \max_{1 \le i \le n} \map {p_i} x$
for each $x \in X_0$.
Define $p : X \to \R_{\ge 0}$ by: 
:$\ds \map p x = C \max_{1 \le i \le n} \map {p_i} x$
for each $x \in X$. 
From Pointwise Maximum of Finite Family of Seminorms is Seminorm and Non-Negative Scalar Multiple of Seminorm on Vector Space is Seminorm, we have that $p$ is a seminorm.
So we have: 
:$\cmod {\map {f_0} x} \le \map p x$
for each $x \in X_0$.
From:
:the Hahn-Banach Theorem: Real Vector Space: Corollary 1 if $\GF = \R$
:the Hahn-Banach Theorem: Complex Vector Space: Corollary if $\GF = \C$
there exists a linear functional $f$ extending $f_0$ such that: 
:$\ds \cmod {\map f x} \le \map p x =  C \max_{1 \le i \le n} \map {p_i} x$ 
for each $x \in X_0$. 
From Characterization of Continuous Linear Transformations between Locally Convex Spaces, $f$ is continuous.
So $f$ is a continuous linear functional satisfying the demand.
{{qed}}
Category:Functional Analysis
Category:Locally Convex Spaces
ffuzm5nkbtcc1b9xrc7lqr30al8eydz
Theorem: Non-Negative Scalar Multiple of Seminorm on Vector Space is Seminorm

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $p$ be a seminorm on $X$.
Let $\alpha \in \R_{\ge 0}$.
Let $q = \alpha p$. 
Then $q$ is a seminorm on $X$.

Proof:
=== {{SeminormAxiom|2}} ===
Let $x \in X$ and $k \in \GF$. 
We have:
{{begin-eqn}}
{{eqn	| l = \map q {k x}
		| r = \alpha \map p {k x}
}}
{{eqn	| r = \alpha \cmod k \map p x
		| c = {{SeminormAxiom|2}} for $p$
}}
{{eqn	| r = \cmod k \map q x
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Norm on Vector Space is Seminorm

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$. 
Let $\norm {\, \cdot \,}$ be a norm on $X$. 
Then $\norm {\, \cdot \,}$ is a seminorm.

Proof:
Note that {{NormAxiomVector|2}} and {{NormAxiomVector|3}} are precisely {{SeminormAxiom|2}} and {{SeminormAxiom|3}}.
{{qed}}
Category:Seminorms
Category:Normed Spaces
ituqwziuvtw1f7cdjuiayolrsbculmt
Theorem: Positive Scalar Multiple of Norm on Vector Space is Norm

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$. 
Let $\alpha > 0$ be a real number. 
Define $\norm {\, \cdot \,}' : X \to \R_{\ge 0}$ by: 
:$\norm x' = \alpha \norm x$
for each $x \in X$.
Then $\norm {\, \cdot \,}'$ is a norm on $X$.

Proof:
=== {{NormAxiomVector|1|nolink}} ===
Suppose that $x \in X$ is such that: 
:$\norm x' = 0$
Then we have: 
:$\alpha \norm x = 0$
Since $\alpha > 0$, it follows that: 
:$\norm x = 0$ 
From {{NormAxiomVector|1}}, we have $x = {\mathbf 0}_X$.
{{qed|lemma}}
Theorem: Locally Convex Space is Topological Vector Space

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \PP}$ be a locally convex space over $\GF$ equipped with the standard topology $\tau$. 
Then $\struct {X, \tau}$ is a topological vector space.

Proof:
From Vector Addition on Locally Convex Space is Continuous, vector addition on $X$ is continuous. 
From Scalar Multiplication on Locally Convex Space is Continuous, scalar multiplication on $X$ is continuous. 
So $\struct {X, \tau}$ is a topological vector space.
{{qed}}
Category:Locally Convex Spaces
Category:Topological Vector Spaces
Category:Locally Convex Space is Topological Vector Space
gj10p4l6th3t9gans3vfecmczf2em84
Theorem: Existence of Non-Zero Continuous Linear Functional vanishing on Proper Closed Subspace of Locally Convex Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \PP}$ be a locally convex space over $\GF$.
Let $Y$ be a proper closed linear subspace of $X$.
Let $x_0 \in X \setminus Y$. 
Then there exists a continuous linear functional $f : X \to \GF$ such that: 
:$\map f y = 0$ for each $y \in Y$
and:
:$\map f {x_0} \ne 0$

Proof:
Let:
:$X_0 = \map \span {Y \cup \set x}$
From Linear Span is Linear Subspace, we have: 
:$X_0$ is a linear subspace of $X$.
Note that we can then write any $u \in X_0$ in the form: 
:$u = y + \alpha x$
for $y \in Y$ and $\alpha \in \mathbb F$. 
We want to define a map in terms of this representation, so we show that this representation is unique. 
Let: 
:$u = y_1 + \alpha_1 x = y_2 + \alpha_2 x$
Then: 
:$\paren {\alpha_2 - \alpha_1} x = y_1 - y_2$
If $\alpha_1 = \alpha_2$, then we have $y_1 = y_2$ as required.
{{AimForCont}} suppose that $\alpha_1 \ne \alpha_2$, then we would have: 
:$\ds x = \frac 1 {\alpha_2 - \alpha_1} \paren {y_1 - y_2}$
and so $x \in Y$, from the definition of a linear subspace, contradiction. 
So, we must have $\alpha_1 = \alpha_2$ and $y_1 = y_2$, and so the representation is unique. 
Now, define $f_0 : X_0 \to \GF$ by: 
:$\map {f_0} {y + \lambda x_0} = \lambda$
for each $y \in Y$, $\lambda \in \GF$.
We have $\map {f_0} x = 0$ {{iff}} $x \in Y$, so that: 
:$\ker f_0 = Y$
This is closed, so by Characterization of Continuous Linear Functionals on Topological Vector Space, we have: 
:$f_0$ is continuous. 
From Hahn-Banach Theorem for Continuous Linear Functional on Locally Convex Space, there exists a continuous linear functional $f$ extending $f_0$. 
Then we have: 
:$\map f {x_0} = \map {f_0} {x_0} = 1 \ne 0$ 
and: 
:$\map f y = \map {f_0} y = 0$
for each $y \in Y$.
So $f$ is a continuous linear functional satisfying our requirements.
{{qed}}
Category:Linear Functionals
Category:Locally Convex Spaces
lsopaqnhv7a3cwybk21ca73ox312u8y
Theorem: Equivalence of Definitions of Metrizable Space/Lemma 1

:$d_\phi$ is a metric on $S$.

Proof:
We note that by definition $d: M \to \R$ is a metric on $M$.
Hence $d$ satisfies all the metric space axioms.
Theorem: Equivalence of Definitions of Metrizable Space/Lemma 2

:$\forall U \subseteq S : U$ is open in $\struct{S, d_\phi}$ {{iff}} $\phi \sqbrk U$ is open in $\struct{A, d}$

Proof:
=== Lemma 3 ===
{{:Equivalence of Definitions of Metrizable Space/Lemma 3}}{{qed|lemma}}
Let $U \subseteq S$.
Theorem: Equivalence of Definitions of Metrizable Space/Lemma 3

:$\forall s \in S, \epsilon \in \R_{\ge 0} : \phi \sqbrk {\map {B_\epsilon} s} = \map {B_\epsilon} {\map \phi s}$
where:
:$(1) \quad \map {B_\epsilon} s$ is the open ball in $\struct{S, d_\phi}$ with center $s$ and radius $\epsilon$
:$(2) \quad \map {B_\epsilon} {\map \phi s}$ is the open ball in $\struct{A, d}$ with center $\map \phi s$ and radius $\epsilon$.

Proof:
Let $s \in S$.
Let $\epsilon \in \R_{\ge 0}$.
We have:
{{begin-eqn}}
{{eqn | l = x \in \map {B_\epsilon} s
      | o = \leadstoandfrom
      | r = \map {d_\phi} {s, x} < \epsilon
      | c = {{Defof|Open Ball}} in $\struct{S, d_\phi}$
}}
{{eqn | o = \leadstoandfrom
      | r = \map d {\map \phi s, \map \phi x} < \epsilon
      | c = Definition of $d_\phi$
}}
{{eqn | o = \leadstoandfrom
      | r = \map \phi x \in \map {B_\epsilon} {\map \phi s}
      | c = {{Defof|Open Ball}} in $\struct{A, d}$
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \phi^{-1} \sqbrk {\map {B_\epsilon} {\map \phi s} }
      | c = {{Defof|Preimage of Mapping}}
}}
{{end-eqn}}
By set equality:
:$\map {B_\epsilon} s = \phi^{-1} \sqbrk {\map {B_\epsilon} {\map \phi s}}$
Hence:
:$\phi \sqbrk {\map {B_\epsilon} s} = \phi \sqbrk {\phi^{-1} \sqbrk {\map {B_\epsilon} {\map \phi s}}}$
By definition of homeomorphism:
:$\phi$ is a surjection
From Image of Preimage of Subset under Surjection equals Subset:
:$\phi \sqbrk {\phi^{-1} \sqbrk {\map {B_\epsilon} {\map \phi s}}} = \map {B_\epsilon} {\map \phi s}$
The result follows.
{{qed}}
Category:Equivalence of Definitions of Metrizable Space
apjmiump6qwai31r3ttj0nxqmdnciqt
Theorem: Linear Combination of Continuous Functions valued in Topological Vector Space is Continuous

Let $X$ be a topological space. 
Let $K$ be a topological field.
Let $Y$ be a topological vector space over $K$. 
Let $n \in \N$.
Let $f_1, \ldots, f_n : X \to Y$ be continuous functions. 
Let $\alpha_1, \ldots, \alpha_n \in K$. 
Then: 
:$\ds \sum_{k \mathop = 1}^n \alpha_k f_k$ is a continuous function.

Proof:
We do induction on the number of functions $n$:
Theorem: Cartesian Space of Topological Field is Topological Vector Space

Let $K$ be a topological field.
Let $K^n$ be the cartesian $n$-th power of $K$, defining scalar multiplication and vector addition component-wise.
Equip $K^n$ with the product topology given by $K$.
Then $K^n$ is a topological vector space. 
{{Refactor|level = medium|extract the following into its own (corollary) page}}
Further, if $K$ is a Hausdorff topological field, then $K^n$ is a Hausdorff topological vector space.

Proof:
If $K$ is Hausdorff, then from Product Space is $T_2$ iff Factor Spaces are $T_2$ the topology on $K^n$ is Hausdorff.
We therefore just need to show that scalar multiplication and vector addition are continuous.
Theorem: Sum of Continuous Functions on Topological Ring is Continuous

Let $X$ be a topological space.
Let $R$ be a topological ring.
Let $f, g : X \to R$ be continuous mappings.
Then $f + g : X \to R$ is continuous.

Proof:
Equip the Cartesian product $R \times R$ with its product topology.
Define $h : X \to R \times R$ by: 
:$\map h x = \tuple {\map f x, \map g x}$ 
for each $x \in X$ and $s : R \times R \to R$ by: 
:$\map s {x, y} = x + y$ 
for each $\tuple {x, y} \in R \times R$. 
From Continuous Mapping to Product Space, $h$ is continuous.
From the definition of a topological ring, $s$ is continuous.
From Composite of Continuous Mappings is Continuous, $s \circ h : X \to R$ is continuous.
Then: 
{{begin-eqn}}
{{eqn | l = \map {\paren {s \circ h} } x
      | r = \map s {\map f x, \map g x}
}}
{{eqn | r = \map f x + \map g x
}}
{{end-eqn}}
for $x \in X$.
{{qed}}
Category:Continuous Mappings (Topology)
Category:Topological Rings
7chrbvl8j673f4wcjyo1yc580r6gezv
Theorem: Product of Continuous Functions on Topological Ring is Continuous

Let $X$ be a topological space. 
Let $R$ be a topological ring. 
Let $f, g : X \to R$ be continuous functions.
Then $f \cdot g : X \to R$ is continuous.

Proof:
Equip the Cartesian product $R \times R$ with its product topology.
Define $h : X \to R \times R$ by: 
:$\map h x = \tuple {\map f x, \map g x}$ 
for each $x \in X$ and $p : R \times R \to R$ by: 
:$\map p {x, y} = x y$
for each $\tuple {x, y} \in R \times R$.
From Continuous Mapping to Product Space, $h$ is continuous.
From the definition of a topological ring, $p$ is continuous.
Then from Composite of Continuous Mappings is Continuous, $p \circ h : X \to R$ is continuous, while: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {p \circ h} } x
		| r = \map p {\map f x, \map g x}
}}
{{eqn	| r = \map f x \map g x
}}
{{end-eqn}}
for $x \in X$.
{{qed}}
Category:Topological Rings
qtg3xkj2f460qwey5c057yp8gbl9l3i
Theorem: Normed Dual Space of Normed Quotient Vector Space is Isometrically Isomorphic to Annihilator

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$.
Let $X^\ast$ be the normed dual space of $X$. 
Let $Y$ be a closed linear subspace of $X$. 
Let $\paren {X/Y}^\ast$ be the normed dual space of the normed quotient vector space $X/Y$.
Then: 
:$\paren {X/Y}^\ast$ is isometrically isomorphic to $Y^\bot$
where $Y^\bot$ is the annihilator of $Y$.

Proof:
Let $\pi$ be the quotient mapping associated with $X/Y$. 
Note that for each $f \in \paren {X/Y}^\ast$ we have: 
:$f \circ \pi \in X^\ast$
by Composition of Bounded Linear Transformations is Bounded Linear Transformation.
Further, for $y \in Y$ we have $\map \pi y = 0_{X/Y}$ from Kernel of Quotient Mapping, and so: 
:$\map {\paren {f \circ \pi} } y = \map f {0_{X/Y} } = 0$ for all $y \in Y$. 
So we have $f \circ \pi \in Y^\bot$.
Now define $\phi : \paren {X/Y}^\ast \to Y^\bot$ by: 
:$\map \phi f = f \circ \pi$ 
From Linear Isometry is Injective: Corollary, it suffices to show that $\phi$ is a linear isometry and surjective.
First, take $f, g \in \paren {X/Y}^\ast$ and $\lambda, \mu \in \GF$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map \phi {\lambda f + \mu g}
		| r = \paren {\lambda f + \mu g} \circ \pi
}}
{{eqn	| r = \lambda \paren {f \circ \pi} + \mu \paren {g \circ \pi}
}}
{{eqn	| r = \lambda \map \phi f + \mu \map \phi g
}}
{{end-eqn}}
so $\phi$ is linear. 
Now, we have for $f \in \paren {X/Y}^\ast$: 
{{begin-eqn}}
{{eqn	| l = \norm {\map \phi f}_{X^\ast}
		| r = \sup_{x \in B_X} \cmod {\map {\paren {f \circ \pi} } x}
		| c = {{Defof|Norm on Bounded Linear Transformation}}
}}
{{eqn	| r = \sup_{\mathbf x \in \map \pi {B_X} } \cmod {\map f {\mathbf x} }
}}
{{eqn	| r = \sup_{\mathbf x \in B_{X/Y} } \cmod {\map f {\mathbf x} }
		| c = Quotient Mapping Maps Unit Open Ball in Normed Vector Space to Unit Open Ball in Normed Quotient Vector Space
}}
{{eqn	| r = \norm f_{X/Y}
		| c = {{Defof|Norm on Bounded Linear Functional}}
}}
{{end-eqn}}
so $\phi$ is a linear isometry.
It remains to show that $\phi$ is surjective. 
Since we have shown that: 
:$\ds \sup_{\mathbf x \in \map \pi {B_X} } \cmod {\map f {\mathbf x} } = \sup_{\mathbf x \in B_{X/Y} } \cmod {\map f {\mathbf x} }$
we know that if $f \circ \pi \in X^\ast$, then $f \in \paren {X/Y}^\ast$.
From Condition for Mapping from Quotient Vector Space to be Well-Defined, we have that for each $g \in X^\ast$, there exists $f : X/Y \to \GF$ such that: 
:$g = f \circ \pi$ 
From the above, it follows that $f \in \paren {X/Y}^\ast$ and so $g = \map \phi f$. 
So $\phi$ is surjective, and we are done from Linear Isometry is Injective: Corollary.
{{qed}}
Theorem: Double Angle Formula for Tangent/Corollary

Let $u = \tan \dfrac \theta 2$.
Then:
:$\tan \theta = \dfrac {2 u} {1 - u^2}$

Proof:
From Double Angle Formula for Tangent:
:$\tan 2 \theta = \dfrac {2 \tan \theta} {1 - \tan^2 \theta}$
The result follows by substituting $\dfrac \theta 2$ for $\theta$.
{{qed}}
Theorem: Linear Transformation from Cartesian Space on Hausdorff Topological Field to Topological Vector Space is Continuous

Let $K$ be a topological field.
Let $K^n$ be the $n$-Cartesian space as a topological vector space with its product topology.
Let $X$ be a topological vector space over $K$.
Let $f : K^n \to X$ be a linear transformation.
Then $f$ is continuous.

Proof:
Let $\set {e_1, \ldots, e_n}$ be the standard basis for $K^n$.
For each $\alpha_1, \alpha_2, \ldots, \alpha_n$ we have: 
:$\ds \map f {\sum_{i \mathop = 1}^n \alpha_i e_i} = \sum_{i \mathop = 1}^n \alpha_i \map f {e_i}$
Let $\pr_i : K^n \to K$ be the projection of $K^n$ onto its $i$th factor, so that: 
:$\ds \map {\pr_i} {\sum_{i \mathop = 1}^n \alpha_i e_i} = \alpha_i$
Then we have: 
:$\ds \map f x = \sum_{i \mathop = 1}^n \map {\pr_i} x \map f {e_i}$ 
for each $x \in K^n$.
From Projection from Product Topology is Continuous:
:$\pr_i$ is continuous for each $1 \le i \le n$. 
From Linear Combination of Continuous Functions valued in Topological Vector Space is Continuous:
:$f$ is continuous.
{{qed}}
Theorem: Balanced Set in Topological Vector Space is Connected

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a topological vector space over $\GF$.
Let $B \subseteq X$ be a balanced set. 
Then $B$ is connected.

Proof:
We first show that $B$ is path connected.
Let $x \in B$. 
Define $p : \closedint 0 1 \to X$ by: 
:$\map p t = t x$
We clearly have: 
:$\map p 0 = 0$
and:
:$\map p 1 = x$ 
Since $B$ is balanced, we have: 
:$t x \in B$
for each $t \in \closedint 0 1$.
It remains to show that $p$ is continuous.
Define $m : \closedint 0 1 \times X$ by:
:$\map m {\lambda, x} = \lambda x$ 
for each $\tuple {\lambda, x} \in \closedint 0 1 \times X$.
From Restriction of Continuous Mapping is Continuous, we have that $m$ is continuous. 
We can then see that $p$ is the $x$-horizontal section of $m$. 
From Horizontal Section of Continuous Function is Continuous, we have that $p$ is continuous.
So every $x \in B$ connects to $0 \in B$.
So from Path-Connected iff Path-Connected to Point, we have that $B$ is path-connected.
From Path-Connected Space is Connected, $B$ is connected.
{{qed}}
Category:Balanced Sets
Category:Connected Topological Spaces
Category:Topological Vector Spaces
jwcl80psra4c54aepz2hvdlokj3szme
Theorem: Isomorphism from Cartesian Space to Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Homeomorphism

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a Hausdorff topological vector space over $\GF$.
Let $n \in \N$. 
Let $Y$ be a subspace of $X$ with dimension $n$. 
Let $f : \GF^n \to Y$ be a vector space isomorphism.
Then $f$ is a homeomorphism.

Proof:
First, we assure ourselves that such a vector space isomorphism $f : \GF^n \to Y$ exists from Same Dimensional Vector Spaces are Isomorphic.
From Linear Transformation from Cartesian Space on Hausdorff Topological Field to Topological Vector Space is Continuous, $f$ is continuous.
It suffices to show that $f^{-1}$ is continuous.
Let $S$ be the unit sphere in $\GF^n$. 
Let $B$ be the unit ball in $\GF^n$. 
From Heine-Borel Theorem: Normed Vector Space, we have that $S$ is compact. 
Let: 
:$K = f \sqbrk S$
From Continuous Image of Compact Space is Compact, $K$ is compact.
From Compact Subspace of Hausdorff Space is Closed, $K$ is closed in $X$.
Note that $\ker f = \set { {\mathbf 0}_X}$, since $f$ is injective, so we have $\mathbf 0_X \not \in K$. 
From Characterization of Closure by Open Sets, there exists an open neighborhood $U$ of $\mathbf 0_X$ such that: 
:$U \cap K = \O$
From Open Neighborhood of Origin in Topological Vector Space contains Balanced Open Neighborhood, there exists a balanced open neighborhood of $\mathbf 0_X$ such that $V \subseteq U$.
From the definition of the subspace topology we then obtain that $V \cap Y$ is a  balanced open neighborhood of $\mathbf 0_X$ in $Y$ such that: 
:$\paren {V \cap Y} \cap K = \O$ 
Now set: 
:$E = f^{-1} \sqbrk {V \cap Y} = f^{-1} \sqbrk V$
This is non-empty, since $0 \in E$.
Further, we show that $E$ and $S$ are disjoint sets.
If $x \in E \cap S$ we would have: 
:$\map f x \in K$
and:
:$\map f x \in E$
But since $E \cap S = \O$, this is impossible.
Since $f$ is linear, $f^{-1}$ is linear by Inverse of Linear Transformation is Linear Transformation. 
Since $V$ is balanced, we have that $E = f^{-1} \sqbrk V$ is balanced from Image of Balanced Set under Linear Transformation is Balanced.
From Balanced Set in Topological Vector Space is Connected, $E$ is connected.
We argue that we must have $E \subseteq B$.
Let $D$ be the closed unit ball in $\GF^n$. 
We can then write: 
:$\GF^n = B \cup S \cup \paren {\GF^n \setminus D}$
So, we may write: 
:$E = \paren {B \cap E} \cup \paren {E \cap \paren {\GF^n \setminus D} }$
from Intersection Distributes over Union, since $E \cap S = \O$. 
Since $\GF^n \setminus D$ is open, if we had: 
:$E \cap \paren {\GF^n \setminus D} \ne \O$ 
then $E$ would be disconnected as the union of disjoint open sets.
We have determined that $E$ is connected, so we have: 
:$E \cap \paren {\GF^n \setminus D} = \O$
and so: 
:$B \cap E = E$
giving:
:$f^{-1} \sqbrk V = E \subseteq B$
From Characterization of von Neumann-Boundedness in Normed Vector Space, we have that $B$ is von Neumann bounded.
So $f^{-1}$ maps an open neighborhood of $\mathbf 0_X$ into a von Neumann bounded set. 
It follows from Characterization of Continuous Linear Functionals on Topological Vector Space that $f^{-1}$ is continuous.
{{qed}}
Theorem: Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Closed

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a Hausdorff topological vector space over $\GF$.
Let $n \in \N$. 
Let $Y$ be a subspace of $X$ with dimension $n$. 
Then $Y$ is closed.

Proof:
Let $f : \GF^n \to Y$ be a vector space isomorphism.
From Isomorphism from Cartesian Space to Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Homeomorphism, $f$ is a homeomorphism. 
Let $B$ be the unit ball in $\GF^n$. 
Let $D$ be the closed unit ball in $\GF^n$. 
Let $S$ be the unit sphere in $\GF^n$ and: 
:$K = f \sqbrk S$  
In Isomorphism from Cartesian Space to Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Homeomorphism, it was determined that there exists a balanced open neighborhood $V$ of $\mathbf 0_X$ such that: 
:$V \cap K = \O$
Now let $\map \cl Y$ be the closure of $Y$. 
From Set is Closed iff Equals Topological Closure, we just need to show that $Y^- \subseteq Y$. 
From Topological Vector Space as Union of Dilations of Open Neighborhood of Origin, there exists $t > 0$ such that: 
:$p \in t V$
It follows that: 
:$p \in \map \cl {Y \cap t V}$
In Isomorphism from Cartesian Space to Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Homeomorphism, it was determined that: 
:$f^{-1} \sqbrk V \subseteq B$
so that: 
:$Y \cap \paren {t V} \subseteq t f \sqbrk B$ 
by Image of Preimage under Mapping.
From Image of Dilation of Set under Linear Transformation is Dilation of Image, we have: 
:$Y \cap \paren {t V} \subseteq f \sqbrk {t B}$
That is: 
:$Y \cap \paren {t V} \subseteq f \sqbrk {t D}$
Since $D$ is compact, we have: 
:$t D$ is compact
from Dilation of Compact Set in Topological Vector Space is Compact.
From Continuous Image of Compact Space is Compact, $f \sqbrk {t D}$ is compact.
Since $X$ is a Hausdorff topological vector space, $X$ is in particular Hausdorff.
From Compact Subspace of Hausdorff Space is Closed, $f \sqbrk {t D}$ is therefore closed, and we obtain: 
:$\map \cl {Y \cap \paren {t V} } \subseteq f \sqbrk {t D}$ 
So: 
:$p \in f \sqbrk {t D}$
giving $p \in Y$. 
So we have $Y^- = Y$ as desired.
{{qed}}