avewright/proofwiki-math huggingface dataset:
Theorem: Classification of Compact Two-Manifolds

A smooth, compact, path-connected manifold of dimension $2$ is diffeomorphic to one of the following:
:the sphere $\mathbb S^2$
:a connected sum of tori $\mathbb T^2$
:a connected sum of projective spaces $\mathbb{RP}^2$.
Such a $2$-manifold with boundary is diffeomorphic to one of the following:
:the sphere $\mathbb S^2$
:a connected sum of tori $\mathbb T^2$
:a connected sum of projective spaces $\mathbb{RP}^2$, with a number of open disks removed.
The Euler characteristic, orientability, and number of boundary curves suffice to describe a surface.

Proof:
It is known that the connected sum of $g$ tori, $\mathbb T_1^2 \# \mathbb T_2^2 \# \ldots \# \mathbb T_g^2$, which we denote $g \mathbb T^2$, is orientable and has Euler characteristic $2 - 2 g - b$, where $b$ is the number of boundary curves.
It is also known that the connected sum of $p$ projective spaces $p \mathbb{RP}^2$ is non-orientable and has Euler characteristic $2 - p - b$.
Thus the Euler characteristic, number of boundary curves and orientability distinguish any closed, path-connected $2$-manifold.
{{explain|All the results referred to above need to be sourced.}}
Theorem: Standard Ordered Basis is Basis

Let $\struct {R, +, \circ}$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $n$ be a positive integer.
For each $j \in \closedint 1 n$, let $e_j$ be the ordered $n$-tuple of elements of $R$ whose $j$th entry is $1_R$ and all of whose other entries is $0_R$.
Then $\sequence {e_n}$ is an ordered basis of the $R$-module $R^n$.
This ordered basis is called the '''standard ordered basis of $R^n$'''.
The corresponding set $\set {e_1, e_2, \ldots, e_n}$ is called the '''standard basis of $R^n$'''.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \lambda_k e_k
      | r = \lambda_1 \tuple {1_R, 0_R, 0_R, \ldots, 0_R}
      | c = 
}}
{{eqn | o = +
      | r = \lambda_2 \tuple {0_R, 1_R, 0_R, \ldots, 0_R}
      | c = 
}}
{{eqn | o = +
      | r = \ldots
      | c = 
}}
{{eqn | o = +
      | r = \lambda_n \tuple {0_R, 0_R, 0_R, \ldots, 1_R}
      | c = 
}}
{{eqn | r = \tuple {\lambda_1, \lambda_2, \lambda_3, \ldots, \lambda_n}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Basis for Finite Submodule of Function Space

Let $\struct {R, +, \circ}$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $A$ be a set.
For each $a \in A$, let $f_a: A \to R$ be defined as:
:$\forall x \in A: \map {f_a} x = \begin{cases}
1 & : x = a \\
0 & : x \ne a
\end{cases}$
Then $B = \set {f_a: a \in A}$ is a basis of the Finite Submodule of Function Space $R^{\paren A}$.

Proof:
Let $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ be a sequence of distinct terms of $A$.
Let $\sequence {\lambda_k}_{1 \mathop \le k \mathop \le n}$ be a sequence of scalars.
Then: $\ds \sum_{k \mathop = 1}^n \lambda_k f_{a_k}$ is the mapping whose value at $a_k$ is $\lambda_k$ and whose value at any $x$ not in $\set {a_1, a_2, \ldots, a_n}$ is zero.
Hence $B$ is a generator of $R^{\paren A}$ which is linearly independent.
Thus, by definition, $B$ is a basis of $R^{\paren A}$.
If $A = \closedint 1 n$, then $B$ is the standard basis of $R^n$.
{{Qed}}
Theorem: Unique Representation by Ordered Basis

Let $G$ be a unitary $R$-module.
Then $\sequence {a_n}$ is an ordered basis of $G$ {{iff}}:
:For every $x \in G$ there exists one and only one sequence $\sequence {\lambda_n}$ of scalars such that $\ds x = \sum_{k \mathop = 1}^n \lambda_k a_k$.

Proof:
=== Necessary Condition ===
Let $\sequence {a_n}$ be an ordered basis of $G$.
Then every element of $G$ is a linear combination of $\set {a_1, \ldots, a_n}$, which is a generator of $G$, by Generated Submodule is Linear Combinations.
Thus there exists at least one such sequence of scalar.
Now suppose there were two such sequences of scalars: $\sequence {\lambda_n}$ and $\sequence {\mu_n}$.
That is, suppose $\ds \sum_{k \mathop = 1}^n \lambda_k a_k = \sum_{k \mathop = 1}^n \mu_k a_k$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \paren {\lambda_k - \mu_k} a_k
      | r = \sum_{k \mathop = 1}^n \paren {\lambda_k a_k - \mu_k a_k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \lambda_k a_k - \sum_{k \mathop = 1}^n \mu_k a_k
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So $\lambda_k = \mu_k$ for all $k \in \closedint 1 n$ as $\sequence {a_n}$ is a linearly independent sequence.
{{qed|lemma}}
Theorem: Isomorphism from R^n via n-Term Sequence

Let $G$ be a unitary $R$-module.
Let $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ be an ordered basis of $G$.
Let $R^n$ be the $R$-module $R^n$.
Let $\psi: R^n \to G$ be defined as:
:$\ds \map \psi {\sequence {\lambda_k}_{1 \mathop \le k \mathop \le n} } = \sum_{k \mathop = 1}^n \lambda_k a_k$
Then $\psi$ is an isomorphism.

Proof:
By Unique Representation by Ordered Basis, $\psi$ is a bijection.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \lambda_k a_k + \sum_{k \mathop = 1}^n \mu_k a_k
      | r = \sum_{k \mathop = 1}^n \paren {\lambda_k a_k + \mu_k a_k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\lambda_k + \mu_k} a_k
      | c = 
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \beta \sum_{k \mathop = 1}^n \lambda_k a_k
      | r = \sum_{k \mathop = 1}^n \beta \paren {\lambda_k a_k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\beta \lambda_k} a_k
      | c = 
}}
{{end-eqn}}
thus proving that $\psi$ is also a homomorphism.
{{Qed}}
Theorem: Unitary R-Modules with n-Element Bases are Isomorphic

Let $G$ and $H$ be unitary $R$-modules for some ring with unity $R$.
Let $G$ and $G$ both have bases with $n$ elements.
Then $G$ and $H$ are isomorphic.

Proof:
From Isomorphism from $R^n$ via $n$-Term Sequence, both $G$ and $H$ are isomorphic to the $R$-module $R^n$.
{{qed}}
Theorem: R-Module R^n is n-Dimensional

The $R$-module $R^n$ is $n$-dimensional.

Proof:
Follows directly from Standard Ordered Basis is Basis.
{{qed}}
Category:Module on Cartesian Product
4e2u0vlwjpxp8kx7zj4kipknso5ie65
Theorem: Linear Transformation from Ordered Basis less Kernel

Let $G$ and $H$ be unitary $R$-modules.
Let $\phi: G \to H$ be a non-zero linear transformation.
Let $G$ be $n$-dimensional.
Let $\sequence {a_n}$ be any ordered basis of $G$ such that $\set {a_k: r + 1 \le k \le n}$ is the basis of the kernel of $\phi$.
Then $\sequence {\map \phi {a_r} }$ is an ordered basis of the image of $\phi$.

Proof:
Suppose:
:$\ds \sum_{k \mathop = 1}^r \lambda_k \map \phi {a_k} = 0$
Then:
:$\ds \map \phi {\sum_{k \mathop = 1}^r \lambda_k a_k} = 0$
So $\ds \sum_{k \mathop = 1}^r \lambda_k \map \phi {a_k}$ belongs to the kernel of $\phi$ and hence is also a linear combination of $\set {a_k: r + 1 \le k \le n}$.
Thus $\forall k \in \closedint 1 r: \lambda_k = 0$ since $\sequence {a_n}$ is linearly independent.
Thus the sequence $\sequence {\map \phi {a_r} }$ is linearly independent.
We have $\forall k \in \closedint {r + 1} n: \map \phi {a_k} = 0$.
So let $x \in G$.
Let $\ds x = \sum_{k \mathop = 1}^n \mu_k a_k$.
Then:
:$\ds \map \phi x = \sum_{k \mathop = 1}^n \mu_k \map \phi {a_k} = \sum_{k \mathop = 1}^r \mu_k \map \phi {a_k}$
Therefore $\sequence {\map \phi {a_r} }$ is an ordered basis of the image of $\phi \sqbrk G$.
{{Qed}}
Theorem: Addition of Linear Transformations

Let $\struct {G, +_G}$ and $\struct {H, +_H}$ be abelian groups.
Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +_G, \circ_G}$ and $\struct {H, +_H, \circ_H}$ be $R$-modules.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Let $\oplus_H$ be defined as pointwise addition on $\map {\LL_R} {G, H}$:
:$\forall \phi, \psi \in \map {\LL_R} {G, H}: \forall x \in G: \map {\paren {\phi \oplus_H \psi} } x := \map \phi x +_H \map \psi x$
Then $\phi \oplus_H \psi: G \to H$ is a linear transformation.

Proof:
From the definition of a module, the group $\struct {H, +_H}$ is abelian.
Hence $\struct {H, +_H}$ is {{afortiori}} a commutative semigroup.
Therefore we can apply Homomorphism on Induced Structure to Commutative Semigroup to show that $\phi +_H \psi: G \to H$ is a homomorphism.
Let $\lambda \in R, x \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {\phi +_H \psi} } {\lambda \circ_G x}
      | r = \map \phi {\lambda \circ_G x} +_H \map \psi {\lambda \circ_G x}
      | c =
}}
{{eqn | r = \lambda \circ_H \map \phi x +_H \lambda \circ_H \map \psi x
      | c =
}}
{{eqn | r = \lambda \circ_H \paren {\map \phi x +_H \map \psi x}
      | c =
}}
{{eqn | r = \lambda \circ_H \map {\paren {\phi +_H \psi} } x
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Negative Linear Transformation

Let $\struct {G, +_G}$ and $\struct {H, +_H}$ be abelian groups.
Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +_G, \circ_G}$ and $\struct {H, +_H, \circ_H}$ be $R$-modules.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Let $\phi: G \to H$ be a linear transformation.
Let $-\phi$ be the pointwise negative of $\phi$:
:$\forall \phi \in \map {\LL_R} {G, H}: \forall x \in G: \map {\paren {-\phi} } x = -\paren {\map \phi x}$
Then $-\phi: G \to H$ is also a linear transformation.

Proof:
From the definition of a module, the group $\struct {H, +_H}$ is abelian.
Therefore we can apply Inverse Mapping in Induced Structure of Homomorphism to Abelian Group to show that $-\phi: G \to H$ is a homomorphism.
Let $\lambda \in R, x \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {-\phi} } {\lambda \circ_G x}
      | r = - \map \phi {\lambda \circ_G x}
      | c =
}}
{{eqn | r = - \lambda \circ_H \map \phi x
      | c =
}}
{{eqn | r = \lambda \circ_H \paren {-\map \phi x}
      | c =
}}
{{eqn | r = \lambda \circ_H \map {\paren {-\phi} } x
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Linear Transformations under Pointwise Addition forms Abelian Group

Let $\struct {G, +_G}$ and $\struct {H, +_H}$ be abelian groups.
Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +_G, \circ}_R$ and $\struct {H, +_H, \circ}_R$ be $R$-modules.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Let $\oplus_H$ be defined as pointwise addition on $\map {\LL_R} {G, H}$:
:$\forall u, v \in \map {\LL_R} {G, H}: \forall x \in G: \map {\paren {u \oplus_H v} } x := \map u x +_H \map v x$
Then $\struct {\map {\LL_R} {G, H}, \oplus_H}$ is an abelian group.

Proof:
From Structure Induced by Group Operation is Group, $\struct {H^G, \oplus_H}$ is a group
Let $\phi, \psi \in \map {\LL_R} {G, H}$.
From Addition of Linear Transformations:
:$\phi \oplus_H \psi \in \map {\LL_R} {G, H}$
From Negative Linear Transformation:
:$-\phi \in \map {\LL_R} {G, H}$
Thus, from the Two-Step Subgroup Test:
:$\struct {\map {\LL_R} {G, H}, \oplus_H}$ is a subgroup of $\struct {H^G, \oplus_H}$.
It remains to be shown that $\struct {\map {\LL_R} {G, H}, \oplus_H}$ is abelian.
Let $u$ and $v$ be arbitrary elements of $\map {\LL_R} {G, H}$.
Indeed, we have that:
{{begin-eqn}}
{{eqn | q = 
      | l = \map {\paren {u \oplus_H v} } x
      | r = \map u x +_H \map v x
      | c = {{Defof|Pointwise Addition of Linear Transformations}}
}}
{{eqn | r = \map v x +_H \map u x
      | c = as $H$ is abelian
}}
{{eqn | r = \map {\paren {v \oplus_H u} } x
      | c = {{Defof|Pointwise Addition of Linear Transformations}}
}}
{{end-eqn}}
{{qed}}
Theorem: Morse-Sard Theorem

Let $f: X \to Y$ be any smooth map of manifolds.
Then almost every point in $Y$ is a regular value of $f$.

Proof:
{{ProofWanted|In progress}}
Theorem: Linear Transformation from Center of Scalar Ring

Let $\struct {G, +_G, \circ}_R$ and $\struct {H, +_H, \circ}_R$ be $R$-modules.
Let $\phi: G \to H$ be a linear transformation.
Let $\map Z R$ be the center of the scalar ring $R$.
Let $\lambda \in \map Z R$.
Then $\lambda \circ \phi$ is a linear transformation.

Proof:
By definition of linear transformation, we need to show that:
:$(1): \quad \forall x, y \in G: \map {\paren {\lambda \circ \phi} } {x +_G y} = \lambda \circ \map \phi x +_H \lambda \circ \map \phi y$
:$(2): \quad \forall x \in G: \forall \mu \in R: \map {\paren {\lambda \circ \phi} } {\mu \circ x} = \mu \circ \map {\paren {\lambda \circ \phi} } x$
Let $\lambda \in \map Z R$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = \map {\paren {\lambda \circ \phi} } {x +_G y}
      | r = \lambda \circ \map \phi {x +_G y}
      | c = 
}}
{{eqn | r = \lambda \circ \paren {\map \phi x +_H \map \phi y}
      | c = 
}}
{{eqn | r = \lambda \circ \map \phi x +_H \lambda \circ \map \phi y
      | c = 
}}
{{eqn | r = \map {\paren {\lambda \circ \phi} } x +_H \map {\paren {\lambda \circ \phi} } y
      | c = 
}}
{{end-eqn}}
Because $\lambda \in \map Z R$, $\lambda$ commutes with all elements of $R$.
So:
:$\forall \mu \in R: \lambda \circ \mu = \mu \circ \lambda$.
Thus:
{{begin-eqn}}
{{eqn | n = 2
      | l = \map {\paren {\lambda \circ \phi} } {\mu \circ x}
      | r = \lambda \circ \map \phi {\mu \circ x}
      | c = 
}}
{{eqn | r = \lambda \circ \mu \circ \map \phi x
      | c = 
}}
{{eqn | r = \mu \circ \lambda \circ \map \phi x
      | c = as $\lambda \in \map Z R$
}}
{{eqn | r = \mu \circ \map {\paren {\lambda \circ \phi} } x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Linear Transformations over Commutative Ring forms Submodule of Module of All Mappings

Let $R$ be a commutative ring.
Let $\struct {G, +_G, \circ}_R$ and $\struct {H, +_H, \circ}_R$ be $R$-modules.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Then $\map {\LL_R} {G, H}$ is a submodule of the $R$-module $H^G$.

Proof:
By definition of abelian group, the center of a commutative ring $R$ is $R$ itself.
So, we need to show that every $\phi \in \map {\LL_R} {G, H}$ fulfils the conditions to be a linear transformation:
:$(1): \quad \forall x, y \in G: \map {\paren {\lambda \circ \phi} } {x +_G y} = \lambda \circ \map \phi x +_H \lambda \circ \map \phi y$
:$(2): \quad \forall x \in G: \forall \mu \in R: \map {\paren {\lambda \circ \phi} } {\mu \circ x} = \mu \circ \map {\paren {\lambda \circ \phi} } x$
for all $\phi \in \map {\LL_R} {G, H}$.
From Linear Transformation from Center of Scalar Ring, these conditions are indeed fulfulled.
Hence the result.
{{qed}}
Theorem: Dimension of Set of Linear Transformations

Let $R$ be a commutative ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $\struct {G, +_G, \circ}_R$ be a unitary $R$-module such that $\map \dim G = n$.
Let $\struct {H, +_H, \circ}_R$ be a unitary $R$-module such that $\map \dim H = m$.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Then:
:$\map \dim {\map {\LL_R} {G, H} } = n m$
where $\map \dim {\map {\LL_R} {G, H} }$ denotes the dimension of $\map {\LL_R} {G, H}$.

Proof:
Consider the set:
:$B = \set {\phi_{i j}: i \in \closedint 1 n, j \in \closedint 1 m}$
From Basis for Set of Linear Transformations, $B$ is a basis for $\map {\LL_R} {G, H}$.
It is seen that by construction, $B$ has $n m$ elements.
The result follows by definition of dimension.
{{Qed}}
Theorem: Dimension of Algebraic Dual

Let $R$ be a commutative ring with unity.
Let $G$ be an $n$-dimensional $R$-module.
Let $G^*$ be the algebraic dual of $G$.
Then $G^*$ is also $n$-dimensional.

Proof:
Let $\struct {R, +_R, \circ}_R$ denote the $R$-module $R$.
From Dimension of $R$-Module $R$ is $1$ we have that the dimension of $\struct {R, +_R, \circ}_R$ is $1$.
By definition, the algebraic dual of $G$ is the $R$-module $\map {\LL_R} {G, R}$ of all linear forms on $G$.
From Dimension of Set of Linear Transformations the dimension of $G^*$ is the product of the dimension of $G$ with the dimension of $\struct {R, +_R, \circ}_R$.
That is:
:$\map \dim {G^*} = n \times 1$
Hence the result.
{{Qed}}
Theorem: Annihilator is Submodule of Algebraic Dual

Let $R$ be a commutative ring with unity.
Let $G$ be a module over $R$.
Let $M$ be a submodule of $G$.
Let $G^*$ be the algebraic dual of $G$.
Then the annihilator $M^\circ$ of $M$ is a submodule of $G^*$.

Proof:
By definition, $M^\circ$ is a subset of $G^*$.
Recall that by definition of algebraic dual, the elements of $G^*$ are linear transformations from $G$ to the $R$-module $R$.
By Submodule Test, it remains to be shown that:
{{begin-eqn}}
{{eqn | n = SM1
      | q = \forall u, v \in M^\circ
      | l = u + v
      | o = \in
      | r = M^\circ
}}
{{eqn | n = SM2
      | q = \forall u \in M^\circ: \forall \lambda \in R
      | l = \lambda u
      | o = \in
      | r = M^\circ
}}
{{end-eqn}}
Indeed:
{{begin-eqn}}
{{eqn | n = SM1
      | q = \forall u, v \in M^\circ: \forall x \in M
      | l = \map u x + \map v x
      | r = 0
      | c = {{Defof|Annihilator on Algebraic Dual}}
}}
{{eqn | ll= \leadsto
      | l = \map {\paren {u + v} } x
      | r = 0
      | c = {{Defof|Pointwise Addition of Linear Transformations}}
}}
{{eqn | ll= \leadsto
      | l = u + v
      | o = \in
      | r = M^\circ
      | c = {{Defof|Annihilator on Algebraic Dual}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | n = SM2
      | q = \forall u \in M^\circ: \forall \lambda \in R: \forall x \in M
      | l = \map {\paren {\lambda u} } x
      | r = 0
      | c = {{Defof|Annihilator on Algebraic Dual}}
}}
{{eqn | ll= \leadsto
      | l = \lambda \map u x
      | r = 0
      | c = {{Defof|Linear Transformation}}
}}
{{eqn | ll= \leadsto
      | l = \lambda u
      | o = \in
      | r = M^\circ
      | c = {{Defof|Annihilator on Algebraic Dual}}
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Evaluation Isomorphism of Annihilator

Let $R$ be a commutative ring with unity.
Let $G$ be a module over $R$ whose dimension is finite.
Let $G^*$ be the algebraic dual of $G$.
Let $G^{**}$ be the algebraic dual of $G^*$.
Let $N$ be a submodule of $G^*$.
Let $J$ be the evaluation isomorphism from $G$ onto $G^{**}$.
Let $N^\circ$ be the annihilator of $N$.
Then:
:$J^{-1} \sqbrk {N^\circ} = \set {x \in G: \forall t \in N: \map t x = 0}$
where $J^{-1} \sqbrk {N^\circ}$ denotes the preimage of $N^\circ$ under $J$.

Proof:
We are given {{hypothesis}} that $G$ is finite-dimensional.
Hence by Evaluation Isomorphism is Isomorphism, $J: G \to G^{**}$ is an isomorphism, and therefore a surjection.
Thus:
:$N^\circ = \set {x^\wedge \in G^{**}: \forall t \in N: \map {x^\wedge} t = 0}$
where $x^\wedge$ is as defined in the definition of the evaluation linear transformation.
The result follows.
{{qed}}
Theorem: Evaluation Linear Transformation is Bilinear

Let $R$ be a commutative ring.
Let $G$ be an $R$-module.
Let $G^*$ be the algebraic dual of $G$.
Let $\innerprod x t$ be the evaluation linear transformation from $G$ to $G^{**}$.
Then the mapping $\phi: G \times G^* \to R$ defined as:
:$\forall \tuple {x, t} \in G \times G^*: \map \phi {x, t} = \innerprod x t$
satisfies the following bilinearity properties:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x, y \in G: \forall t \in G^*
      | l = \innerprod {x + y} t
      | r = \innerprod x t + \innerprod y t
}}
{{eqn | n = 2
      | q = \forall x \in G: \forall s, t \in G^*
      | l = \innerprod x {s + t}
      | r = \innerprod x s + \innerprod x t
}}
{{eqn | n = 3
      | q = \forall x \in G: \forall t \in G^*: \forall \lambda \in R
      | l = \innerprod {\lambda x} t
      | r = \lambda \innerprod x t
}}
{{eqn | r = \innerprod x {\lambda t}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x, y \in G: \forall t \in G^*
      | l = \innerprod {x + y} t
      | r = \map t {x + y}
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{eqn | r = \map t x + \map t y
      | c = $t$ is a Linear Transformation
}}
{{eqn | r = \innerprod x t + \innerprod y t
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | q = \forall x \in G: \forall s, t \in G^*
      | l = \innerprod x {s + t}
      | r = \map {\paren {s + t} } x
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{eqn | r = \map s x + \map t x
      | c = {{Defof|Pointwise Addition of Linear Transformations}}
}}
{{eqn | r = \innerprod x s + \innerprod x t
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 3
      | q = \forall x \in G: \forall t \in G^*: \forall \lambda \in R
      | l = \innerprod {\lambda x} t
      | r = \map t {\lambda x}
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{eqn | r = \lambda \map t x
      | c = $t$ is a Linear Transformation
}}
{{eqn | r = \lambda \innerprod x t
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | n = 3
      | q = \forall x \in G: \forall t \in G^*: \forall \lambda \in R
      | l = \innerprod {\lambda x} t
      | r = \map t {\lambda x}
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{eqn | r = \map {\paren {\lambda t} } x
      | c = $t$ is a Linear Transformation
}}
{{eqn | r = \innerprod x {\lambda t}
      | c = {{Defof|Evaluation Linear Transformation/Module Theory}}
}}
{{end-eqn}}
{{qed}}
Theorem: Zero Vector Space Product iff Factor is Zero

Let $\struct {F, +_F, \times_F}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\struct {\mathbf V, +_V, \ast}_F$ be a vector space over $F$, as defined by the vector space axioms.
Let $\mathbf v \in \mathbf V, \lambda \in F$.
Then:
:$\lambda \ast \mathbf v = \bszero \iff \paren {\lambda = 0_F \lor x = \bszero}$

Proof:
A vector space is a module, so all results about modules also apply to vector spaces.
So from Scalar Product with Identity it follows directly that:
:$\lambda = 0_F \lor \mathbf v = e \implies \lambda \ast \mathbf v = \bszero$
Next, suppose $\lambda \ast \mathbf v = \bszero$ but $\lambda \ne 0_F$.
Then:
{{begin-eqn}}
{{eqn | l = \bszero
      | r = \lambda^{-1} \ast \bszero
      | c = Zero Vector Scaled is Zero Vector
}}
{{eqn | r = \lambda^{-1} \ast \paren {\lambda \ast \mathbf v}
      | c = as $\lambda \ast \mathbf v = \bszero$
}}
{{eqn | r = \paren {\lambda^{-1} \times_F \lambda} \ast \mathbf v
      | c = {{Vector-space-axiom|3}}
}}
{{eqn | r = 1_F \ast \mathbf v
      | c = {{Field-axiom|M4}}
}}
{{eqn | r = \mathbf v
      | c = {{Vector-space-axiom|4}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Zero Vector Space Product iff Factor is Zero

Let $\struct {F, +_F, \times_F}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\struct {\mathbf V, +_V, \ast}_F$ be a vector space over $F$, as defined by the vector space axioms.
Let $\mathbf v \in \mathbf V, \lambda \in F$.
Then:
:$\lambda \ast \mathbf v = \bszero \iff \paren {\lambda = 0_F \lor x = \bszero}$

Proof:
The sufficient condition is proved in Vector Scaled by Zero is Zero Vector, and in Zero Vector Scaled is Zero Vector.
The necessary condition is proved in Vector Product is Zero only if Factor is Zero.
{{qed}}
Theorem: Homomorphic Image of Vector Space

Let $\struct {K, +_K, \times_K}$ be a division ring.
Let $\struct {V, +_V, \circ_V}_K$ be a $K$-vector space.
Let $\struct {W, +_W, \circ_W}_K$ be a $K$-algebraic structure.
Let $\phi: V \to W$ be a homomorphism, that is, a linear transformation.
Then the homomorphic image of $\phi$ is a $K$-vector space.

Proof:
Let us write $\phi \sqbrk V$ for the homomorphic image of $\phi$.
From Homomorphic Image of R-Module is R-Module, $\phi \sqbrk V$ is a $K$-module.
It thus suffices to show that $\phi \sqbrk V$ is unitary, since then it will be a $K$-vector space.
To this end, let $1_K$ be the unity of $K$.
Then for any $\map \phi {\mathbf v} \in \phi \sqbrk V$, compute:
{{begin-eqn}}
{{eqn | l = 1_K \circ_W \map \phi {\mathbf v}
      | r = \map \phi {1_K \circ_V \mathbf v}
      | c = $\phi$ is a linear transformation
}}
{{eqn | r = \map \phi {\mathbf v}
      | c = $V$ is a $K$-vector space
}}
{{end-eqn}}
Hence $\phi \sqbrk V$ is unitary, and so a $K$-vector space.
{{qed}}
Theorem: Direct Product of Vector Spaces is Vector Space

Let $K$ be a field.
Let $V_1, V_2, \ldots, V_n$ be $K$-vector spaces.
Let $\struct {V, + , \circ}_K$ be their direct product.
Then $\struct {V, + , \circ}_K$ is a $K$-vector space.

Proof:
This follows directly from Finite Direct Product of Modules is Module and the definition of vector space.