avewright/proofwiki-math huggingface dataset:
Theorem: Positive Part of Multiple of Function

Let $X$ be a set.
Let $f : X \to \overline \R$ be an extended real-valued function.
Let $\alpha$ be a real number. 
Then:
:$\ds \paren {\alpha f}^+ = \begin{cases}\alpha f^+ & \alpha \ge 0 \\ -\alpha f^- & \alpha < 0\end{cases}$
where:
:$\paren {\alpha f}^+$ and $f^+$ are the positive parts of $\alpha f$ and $f$ respectively
:$f^-$ is the negative part of $f$.

Proof:
Let $x \in X$. 
First take $\alpha \ge 0$.
Suppose that $\map f x \ge 0$.
Then $\alpha \map f x \ge 0$.
So:
:$\max \set {\alpha \map f x, 0} = \alpha \map f x$
and:
:$\max \set {\map f x, 0} = \map f x$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^+} x = \alpha \map f x$
and: 
:$\map {f^+} x = \map f x$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map {f^+} x$
if $\map f x \ge 0$. 
Now suppose that $\map f x < 0$.
Then $\alpha \map f x < 0$.
So:
:$\max \set {\map f x, 0} = 0$
and:
:$\max \set {\alpha \map f x, 0} = 0$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^+} x = 0$
and:
:$\map {f^+} x = 0$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map {f^+} x$
if $\map f x < 0$.
So:
:$\paren {\alpha f}^+ = \alpha f^+$
if $\alpha \ge 0$. 
Now take $\alpha < 0$.
Suppose that $\map f x \ge 0$. 
Then $\alpha \map f x \le 0$. 
So:
:$\max \set {\alpha \map f x, 0} = 0$
and:
:$-\min \set {\map f x, 0} = 0$
So by the definition of the positive part and negative part, we have: 
:$\map {\paren {\alpha f}^+} x = 0$
and:
:$\map {f^-} x = 0$
So:
:$\map {\paren {\alpha f}^+} x = -\alpha \map {f^-} x$
if $\map f x \ge 0$. 
Now suppose that $\map f x < 0$.
Then $\alpha \map f x > 0$.
So:
:$\max \set {\alpha \map f x, 0} = \alpha \map f x$
and:
:$-\min \set {\map f x, 0} = -\map f x$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map f x$
and:
:$\map {f^-} x = -\map f x$
So:
:$\map {\paren {\alpha f}^+} x = -\alpha \map {f^-} x$ 
if $\map f x < 0$. 
So:
:$\paren {\alpha f}^+ = -\alpha f^-$
if $\alpha < 0$. 
{{qed}}
Category:Positive Parts
hz13oduv5ewl6923g8tp6wi1gohmw8o
Theorem: Negative Part of Multiple of Function

Let $X$ be a set.
Let $f : X \to \overline \R$ be an extended real-valued function.
Let $\alpha$ be a real number. 
Then:
:$\ds \paren {\alpha f}^- = \begin{cases}\alpha f^- & \alpha \ge 0 \\ -\alpha f^+ & \alpha < 0\end{cases}$
where:
:$\paren {\alpha f}^-$ and $f^-$ are the negative parts of $\alpha f$ and $f$ respectively
:$f^+$ is the positive part of $f$.

Proof:
Let $x \in X$. 
First take $\alpha \ge 0$.
Suppose that $\map f x \ge 0$.
Then $\alpha \map f x \ge 0$.
So:
:$-\min \set {\alpha \map f x, 0} = 0$
and:
:$-\min \set {\map f x, 0} = 0$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^-} x = 0$
and:
:$\map {f^-} x = 0$
So:
:$\map {\paren {\alpha f}^-} x = \alpha \map {f^-} x$
if $\map f x \ge 0$.
Now suppose that $\map f x < 0$.
Then $\alpha \map f x < 0$.
Then: 
:$-\min \set {\map f x, 0} = -\map f x$
and:
:$-\min \set {\alpha \map f x, 0} = -\alpha \map f x$ 
So by the definition of the positive part and negative part, we have:
:$\map {f^-} x = -\map f x$
and:
:$\map {\paren {\alpha f}^-} x = -\alpha \map f x$
So:
:$\map {\paren {\alpha f}^-} x = \alpha \map {f^-} x$
if $\map f x < 0$.
So: 
:$\paren {\alpha f}^- = \alpha f^-$
if $\alpha \ge 0$. 
Now take $\alpha < 0$. 
Suppose that $\map f x \ge 0$.
Then $\alpha \map f x \le 0$.
Then: 
:$-\min \set {\alpha \map f x, 0} = -\alpha \map f x$
and:
:$\max \set {\map f x, 0} = \map f x$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^-} x = -\alpha \map f x$
and:
:$\map {f^+} x = \map f x$
So:
:$\map {\paren {\alpha f}^-} x = -\alpha \map {f^+} x$
if $\map f x \ge 0$.
Now suppose that $\map f x < 0$.
Then $\alpha \map f x > 0$.
We then have: 
:$-\min \set {\alpha \map f x, 0} = 0$
and: 
:$\max \set {\map f x, 0} = 0$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^-} x = 0$
and:
:$\map {f^-} x = 0$
So:
:$\map {\paren {\alpha f}^-} x = -\alpha \map {f^+} x$
if $\map f x < 0$.
So: 
:$\paren {\alpha f}^- = -\alpha f^+$
if $\alpha \ge 0$. 
{{qed}}
Category:Negative Parts
8g0oavfanxwfscgbnclx05n67c4jcgn
Theorem: Pointwise Scalar Multiple of Measurable Function is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f : X \to \overline \R$ be a $\Sigma$-measurable function.
Let $\alpha \in \overline \R$ be an extended real number. 
Then the pointwise scalar multiple $\alpha f$ is $\Sigma$-measurable.

Proof:
We want to show that: 
:$\set {x \in X : \alpha \map f x \le t}$ is $\Sigma$-measurable for each $t \in \R$.
in each of the cases: 
:$(1): \quad$ $\alpha = 0$
:$(2): \quad$ $0 < \alpha < \infty$
:$(3): \quad$ $-\infty < \alpha < 0$
:$(4): \quad$ $\alpha = \infty$
:$(5): \quad$ $\alpha = -\infty$
If $\alpha = 0$, then $\alpha f = 0$, and $\alpha f$ is $\Sigma$-measurable from Constant Function is Measurable, giving case $(1)$. 
Suppose that $0 < \alpha < \infty$. 
Since $f$ is $\Sigma$-measurable, we have that: 
:$\ds \set {x \in X : \map f x \le \frac t \alpha}$ is $\Sigma$-measurable for each $t \in \R$. 
Since: 
:$\ds \set {x \in X : \alpha \map f x \le t} = \set {x \in X : \map f x \le \frac t \alpha}$
we have the theorem in the case $\alpha > 0$, giving case $(2)$. 
Suppose that $-\infty < \alpha < 0$.
Since $f$ is $\Sigma$-measurable, we have from Characterization of Measurable Functions:
:$\ds \set {x \in X :\map f x \ge \frac t \alpha}$ is $\Sigma$-measurable for each $t \in \R$.
Since:
:$\ds \set {x \in X : \alpha \map f x \le t} = \set {x \in X :\map f x \ge \frac t \alpha}$
we have the theorem in the case $\alpha < 0$, giving case $(3)$. 
Suppose that $\alpha = \infty$.
Then from the definition of extended real multiplication, we have: 
:$\map {\paren {\alpha f} } x = \begin{cases}\infty & \map f x \ne 0 \\ 0 & \map f x = 0\end{cases}$ 
If $t < 0$, we have: 
:$\set {x \in X : \alpha \map f x \le t} = \O$
which is $\Sigma$-measurable.
If $t \ge 0$, we have: 
:$\set {x \in X : \alpha \map f x \le t} = \set {x \in X : \map f x = 0}$
From Measurable Functions Determine Measurable Sets and Constant Function is Measurable, we have that: 
:$\set {x \in X : \map f x = 0} \in \Sigma$
So:
:$\set {x \in X : \alpha \map f x \le t}$ is $\Sigma$-measurable for each $t \in \R$
giving case $(4)$. 
Suppose that $\alpha = -\infty$.
From the rules of extended real multiplication, we have: 
:$\paren {-\infty} \times f = -\paren {\infty \times f}$ 
From case $(4)$, we have that: 
:$\infty \times f$ is $\Sigma$-measurable. 
From case $(2)$, we then have: 
:$\paren {-1} \times \paren {\infty \times f} = \paren {-\infty} \times f$ is $\Sigma$-measurable
hence showing case $(5)$.
{{qed}}
Category:Measurable Functions
1985xplibcdvcj6gobdsros0462crbh
Theorem: Characterization of Essentially Bounded Functions

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \R$ be a $\Sigma$-measurable function.
{{TFAE}}
:$(1) \quad$ $f$ is essentially bounded.
:$(2) \quad$ There exists a bounded function $g : X \to \R$ such that $f = g$ $\mu$-almost everywhere.

Proof:
=== $(1)$ implies $(2)$ ===
Suppose that there exists $c \in \R$ such that: 
:$\map \mu {\set {x \in X : \size {\map f x} > c} } = 0$
Let:
:$A = \set {x \in X : \size {\map f x} \le c}$
Define a function $g : X \to \overline \R$ by: 
:$\map g x = \begin{cases}\map f x & x \in A \\ 0 & x \not \in A\end{cases}$
Then:
:$\size {\map g x} \le c$ for all $x \in X$. 
So:
:$g$ is bounded.
Then if $x \in X$ is such that $\map f x \ne \map g x$, we must have $x \in X \setminus A$.
But {{hypothesis}}:
:$\map \mu {X \setminus A} = \map \mu {\set {x \in X : \size {\map f x} > c} } = 0$
So:
:$f = g$ $\mu$-almost everywhere.
{{qed|lemma}}
Theorem: Triangle Inequality for Integrals/Complex Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\struct {\C, \map \BB \C}$ be the complex numbers made into a measurable space with its Borel $\sigma$-algebra.
Let $f : X \to \C$ be a $\mu$-integrable function.
Then $\cmod f$ is $\mu$-integrable and:
:$\ds \cmod {\int f \rd \mu} \le \int \cmod f \rd \mu$

Proof:
Let $\struct {\R, \map \BB \R}$ be the real numbers made into a measurable space with its Borel $\sigma$-algebra.
From Complex Modulus of Measurable Function is Measurable, $\cmod f$ is $\Sigma/\map \BB \R$-measurable.
We have:
{{begin-eqn}}
{{eqn	| l = \size {\map \Re f}^2 + \size {\map \Im f}^2
		| o = \le 
		| r = \size {\map \Re f}^2 + 2 \size {\map \Re f} \size {\map \Im f} + \size {\map \Im f}^2 
}}
{{eqn	| r = \paren {\size {\map \Re f} + \size {\map \Im f} }^2 
}}
{{end-eqn}}
Taking square roots, we have:
:$\cmod f \le \size {\map \Re f} + \size {\map \Im f}$
Since $f$ is $\mu$-integrable, $\map \Re f$ and $\map \Im f$ are $\mu$-integrable.
From Characterization of Integrable Functions, $\cmod {\map \Re f}$ and $\cmod {\map \Im f}$ are $\mu$-integrable.
Hence from Integral of Integrable Function is Additive, $\size {\map \Re f} + \size {\map \Im f}$ is $\mu$-integrable.
From Characterization of Integrable Functions, $\cmod f$ is then $\mu$-integrable.
Now, let:
:$\ds z = \int f \rd \mu \in \C$
By Complex Multiplication as Geometrical Transformation, there is a complex number $\alpha$ with $\cmod \alpha = 1$ such that:
:$\alpha z = \cmod z \in \R$
Let $u = \map \Re {\alpha f}$.
We have:
:$\ds \alpha \int f \rd \mu = \int \alpha f \rd \mu$
from Integral of Integrable Function is Homogeneous: Complex Function.
Since:
:$\ds \int \alpha f \rd \mu = \cmod {\int f \rd \mu} \in \R$
we have that:
:$\ds \map \Im {\int \alpha f \rd \mu} = \int \map \Im {\alpha f} \rd \mu = 0$ 
Hence:
:$\ds \int \alpha f \rd \mu = \map \Re {\int \alpha f \rd \mu} = \int \map \Re {\alpha f} \rd \mu = \int u \rd \mu$
By Modulus Larger than Real Part, we have that:
:$u \le \cmod {\alpha f} = \cmod f$
Hence by Integral of Integrable Function is Monotone, we have:
:$\ds \int u \rd \mu \le \int \cmod f \rd \mu$ 
Putting everything together we have:
:$\ds \cmod {\int f \rd \mu} \le \int \cmod f \rd \mu$ 
{{qed}}
Category:Triangle Inequality for Integrals
5yfvx2depkuyq9dte3n53m383pv9ahj
Theorem: Dimension of Double Dual

Let $G^{**}$ be the double dual of $G$.
Then $G^{**}$ is also $n$-dimensional.

Proof:
By definition, the double dual of $G$ is the algebraic dual of the algebraic dual $G^*$ of $G$.
From Dimension of Algebraic Dual:
:$\map \dim {G^**} = \map \dim {G^*}$
Also from Dimension of Algebraic Dual::
:$\map \dim {G^*} = \map \dim G$
Hence the result.
{{Qed}}
Theorem: Set of Points at which Sequence of Measurable Functions does not Converge to Given Measurable Function is Measurable

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \R$ be a $\Sigma$-measurable function.
For each $n \in \N$, let $f_n : X \to \R$ be a $\Sigma$-measurable function.
Then:
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x}$ is $\Sigma$-measurable.

Proof:
From Expression for Set of Points at which Sequence of Functions does not Converge to Given Function, we have: 
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x} = \bigcup_{k \mathop = 1}^\infty \bigcap_{N \mathop = 1}^\infty \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$
From Pointwise Difference of Measurable Functions is Measurable, we have: 
:$f_n - f$ is $\Sigma$-measurable for each $n \in \N$.
From Absolute Value of Measurable Function is Measurable, we have: 
:$\size {f_n - f}$ is $\Sigma$-measurable for each $n \in \N$.
From Characterization of Measurable Functions, we have that: 
:$\ds \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$ is $\Sigma$-measurable for each $k, n \in \N$.
Since $\sigma$-Algebras are closed under countable union, we have: 
:$\ds \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$ is $\Sigma$-measurable for each $k, N \in \N$.
Then, from Sigma-Algebra Closed under Countable Intersection: 
:$\ds \bigcap_{N \mathop = 1}^\infty \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$ is $\Sigma$-measurable for each $k \in \N$.
Again, since Since $\sigma$-Algebras are closed under countable union, we have: 
:$\ds \bigcup_{k \mathop = 1}^\infty \bigcap_{N \mathop = 1}^\infty \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$ is $\Sigma$-measurable.
So:
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x}$ is $\Sigma$-measurable.
{{qed}}
Category:Measurable Functions
Category:Convergence
fz69xq6vvalqom4poe3945zddaqdbec
Theorem: Pointwise Convergence implies Convergence Almost Everywhere

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \R$ be a $\Sigma$-measurable function.
For each $n \mathop \in \N$, let $f_n : X \to \R$ be a $\Sigma$-measurable function.
Then:
:if $\sequence {f_n}_{n \mathop \in \N}$ converges pointwise to $f$, it converges almost everywhere to $f$.

Proof:
If $\sequence {f_n}_{n \mathop \in \N}$ converges pointwise to $f$, then: 
:$\sequence {\map {f_n} x}_{n \mathop \in \N}$ converges to $\map f x$ for each $x \in X$. 
So:
:$\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x} = \O$
From Measure of Empty Set is Zero, we have: 
:$\map \mu \O = 0$
So:
:$\map \mu {\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x} } = 0$
So:
:$\sequence {f_n}_{n \mathop \in \N}$ converges almost everywhere to $f$.
{{qed}}
Category:Convergence Almost Everywhere
m13cfpkbo7zlh3ol31adm7i7jkktd0n
Theorem: Convergence in Mean implies Convergence in Measure

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \R$ be a $\Sigma$-measurable function.
For each $n \mathop \in \N$, let $f_n : X \to \R$ be a $\Sigma$-measurable function.
Then:
:if $\sequence {f_n}_{n \mathop \in \N}$ converges in mean to $f$, it converges in measure to $f$.

Proof:
From Pointwise Difference of Measurable Functions is Measurable:
:$f_n - f$ is $\Sigma$-measurable for each $n \in \N$. 
Let $\epsilon > 0$ be a real number.
From Markov's Inequality, we then have: 
:$\ds \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } \le \frac 1 \epsilon \int \size {f_n - f} \rd \mu$
Since $\sequence {f_n}_{n \mathop \in \N}$ converges in mean to $f$, we have: 
:$\ds \lim_{n \mathop \to \infty} \frac 1 \epsilon \int \size {f_n - f} \rd \mu = 0$
So, from the Squeeze Theorem, we have: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } = 0$
for each $\epsilon > 0$.
So:
:$\sequence {f_n}_{n \mathop \in \N}$ converges in measure to $f$.
{{qed}}
Category:Convergence in Mean
Category:Convergence in Measure
gvptyc0fusfmpkct7l0iev51awuorbj
Theorem: Basis for R-Module R

Let $\struct {R, +, \times}$ be a ring with unity whose unity is $1_R$.
Let $\struct {R, +_R, \circ}_R$ denote the $R$-module $R$.
Then $\set {1_R}$ is a basis for $\struct {R, +_R, \circ}_R$.

Proof:
From Dimension of $R$-Module $R$ is $1$ we have that $\struct {R, +_R, \circ}_R$ is $1$-dimensional.
From Standard Ordered Basis is Basis it follows directly that $\set {1_R}$ is a basis for $\struct {R, +_R, \circ}_R$.
{{qed}}
Theorem: Basis for 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$.
Let $\sequence {a_n}$ be an ordered basis for $G$.
Let $\sequence {b_m}$ be an ordered basis for $H$.
Let $\phi_{i j}: G \to H$ be the unique linear transformation defined for each $i \in \closedint 1 n, j \in \closedint 1 m$ which satisfies:
:$\forall k \in \closedint 1 n: \map {\phi_{i j} } {a_k} = \delta_{i k} b_j$
where $\delta$ is the Kronecker delta.
Then:
:$\set {\phi_{i j}: i \in \closedint 1 n, j \in \closedint 1 m}$
is a basis for $\map {\LL_R} {G, H}$.

Proof:
Let $B = \set {\phi_{i j}: i \in \closedint 1 n, j \in \closedint 1 m}$.
Let $\ds \sum_{j \mathop = 1}^m \sum_{i \mathop = 1}^n \lambda_{i j} \phi_{i j} = 0$.
Then:
:$\ds \forall k \in \closedint 1 n: 0 = \sum_{j \mathop = 1}^m \sum_{i \mathop = 1}^n \lambda_{i j} \map {\phi_{i j} } {a_k} = \sum_{j \mathop = 1}^m \lambda_{k j} b_j$
So:
:$\forall j \in \closedint 1 n: \lambda_{k j} = 0$
Hence $B$ is linearly independent.
Now let $\phi \in \map {\LL_R} {G, H}$.
Let $\tuple {\alpha_{i 1}, \alpha_{i 2}, \ldots, \alpha_{i m} }$ be the sequence of scalars that satisfies:
:$\ds \forall i \in \closedint 1 n: \map \phi {a_i} = \sum_{j \mathop = 1}^m \alpha_{i j} b_j$
Then:
:$\ds \forall k \in \closedint 1 n: \map \phi {a_k} = \map {\paren {\sum_{j \mathop = 1}^m \sum_{i \mathop = 1}^n \alpha_{i j} u_{i j} } } {a_k}$
by a calculation similar to the preceding.
So, by Linear Transformation of Generated Module:
:$\ds u = \sum_{j \mathop = 1}^m \sum_{i \mathop = 1}^n \alpha_{i j} u_{i j}$
Thus $B$ is a generator for $\phi \in \map {\LL_R} {G, H}$.
{{Qed}}
Theorem: Dimension of R-Module R is 1

Let $\struct {R, +, \times}$ be a ring whose unity is $1_R$.
Let $\struct {R, +_R, \circ}_R$ denote the $R$-module $R$.
Then the dimension of $\struct {R, +_R, \circ}_R$ is $1$.

Proof:
{{improve|This proof applies only for a ring with unity. Needs to be expanded to any ring.}}
We have by definition that the $R$-module $R$ is the special case of the $R$-module $R^n$ where $n = 1$.
From $R$-module $R^n$ is $n$-Dimensional it follows that $\struct {R, +_R, \circ}_R$ is $1$-dimensional.
{{qed}}
Category:Module on Cartesian Product
2ywhui41riegnvsykfvwazg5rgfclwx
Theorem: Underlying Mapping of Evaluation Linear Transformation is Element of Double Dual

Let $\struct {R, +, \times}$ be a commutative ring with unity.
Let $G$ be an $R$-module.
Let $G^*$ be the algebraic dual of $G$.
Let $G^{**}$ be the double dual of $G$.
For each $x \in G$, let $x^\wedge: G^* \to R$ be defined as:
:$\forall t \in G^*: \map {x^\wedge} t = \map t x$
Then:
:$x^\wedge \in G^{**}$

Proof:
We have that $x^\wedge$ is a mapping from $G^* \to R$.
It remains to be demonstrates that $x^\wedge$ is in fact a linear transformation.
Hence we need to show that:
:$(1): \quad \forall u, v \in G^*: \map {x^\wedge} {u + v} = \map {x^\wedge} u + \map {x^\wedge} v$
:$(2): \quad \forall u \in G^*: \forall \lambda \in R: \map {x^\wedge} {\lambda \times u} = \lambda \times \map {x^\wedge} u$
Hence:
{{begin-eqn}}
{{eqn | n = 1
      | l = \map {x^\wedge} {u + v}
      | r = \map {\paren {u + v} } t
      | c = Definition of $x^\wedge$
}}
{{eqn | r = \map u t + \map v t
      | c = {{Defof|Pointwise Addition of Linear Transformations}}
}}
{{eqn | r = \map {x^\wedge} u + \map {x^\wedge} v
      | c = Definition of $x^\wedge$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | n = 2
      | l = \map {x^\wedge} {\lambda \times u}
      | r = \map {\paren {\lambda \times u} } t
      | c = Definition of $x^\wedge$
}}
{{eqn | r = \lambda \times \map u t
      | c = {{Defof|Linear Transformation}}
}}
{{eqn | r = \lambda \times \map {x^\wedge} u
      | c = Definition of $x^\wedge$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Set of Linear Transformations over Commutative Ring forms Submodule of Module of All Mappings/Unitary

Let $\struct {H, +_H, \circ}_R$ be a unitary module.
Then $\map {\LL_R} {G, H}$ is also a unitary module.

Proof:
From Set of Linear Transformations over Commutative Ring forms Submodule of Module of All Mappings, $\map {\LL_R} {G, H}$ is a module.
It remains to be shown that $\map {\LL_R} {G, H}$ is a unitary module, that is:
:$\forall \phi \in \map {\LL_R} {G, H}: 1_R \circ \phi = \phi$
So, let $\struct {H, +_H, \circ}_R$ be a unitary $R$-module.
Then, by {{Module-axiom|4}}:
:$\forall x \in H: 1_R \circ x = x$
Thus:
{{begin-eqn}}
{{eqn | l = \map {\paren {1_R \circ \phi} } x
      | r = 1_R \circ \paren {\map \phi x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \phi x
      | c = {{Module-axiom|4}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Annihilator is Submodule of Algebraic Dual/Corollary

Let $N$ be a submodule of $G^*$.
Let $G^{**}$ be the algebraic dual of $G^*$.
Then the annihilator $N^\circ$ of $N$ is a submodule of $G^{**}$.

Proof:
Follows directly as an example of Annihilator is Submodule of Algebraic Dual.
{{qed}}
Theorem: Dimension of Annihilator on Algebraic Dual

:$M^\circ$ is an $\paren {n - m}$-dimensional subspace of $G^*$.

Proof:
Let $\sequence {a_n}$ be an ordered basis of $G$ such that $\sequence {a_m}$ is an ordered basis of $M$.
Let $\sequence { {a_n}'}$ be the ordered dual basis of $G^*$.
Let $\ds t = \sum_{k \mathop = 1}^n \lambda_k {a_k}' \in M^\circ$.
Then:
{{begin-eqn}}
{{eqn | q = \forall j \in \closedint 1 m
      | l = \lambda_j
      | r = \map {\sum_{k \mathop = 1}^n \lambda_k {a_k}'} {a_j}
      | c = 
}}
{{eqn | r = \map {\paren {\sum_{k \mathop = 1}^n \lambda_k {a_k}'} } {a_j}
      | c = 
}}
{{eqn | r = \map t {a_j}
      | c = {{hypothesis}}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So $t$ is a linear combination of $\set { {a_k}': m + 1 \le k \le n}$.
But ${a_k}'$ clearly belongs to $M^\circ$ for each $k \in \closedint {m + 1} n$.
Therefore $M^\circ$ has dimension $n - m$.
{{qed}}
Theorem: Annihilator of Annihilator on Algebraic Dual of Subspace is Image under Evaluation Isomorphism

:$M^{\circ \circ} = J \sqbrk M$
where $J \sqbrk M$ denotes the image of $M$ under $J$.

Proof:
Let Dimension of Annihilator on Algebraic Dual be applied to $M^\circ$ instead of $M$.
It is seen that the annihilator $M^{\circ \circ}$ of $M^\circ$ has dimension $n - \paren {n - m} = m$.
But clearly:
:$J \sqbrk M \subseteq M^{\circ \circ}$.
As $J$ is an isomorphism, $J \sqbrk M$ has dimension $m$.
So by Dimension of Proper Subspace is Less Than its Superspace:
:$J \sqbrk M = M^{\circ \circ}$.
As a consequence:
:$\map {J^\gets} {M^{\circ \circ} } = M$
Hence the result:
:$M^{\circ \circ} = J \sqbrk M$
{{qed}}
Theorem: Mapping to Annihilator on Algebraic Dual is Bijection

Let $G_m$ denote the set of all $m$-dimensional subspaces of $G$.
Let ${G^*}_{n - m}$ denote the set of all $n - m$-dimensional subspaces of $G^*$.
Let $\phi: G_m \to {G^*}_{n - m}$ be the mapping from $G_m$ to the power set of ${G^*}_{n - m}$ defined as:
:$\forall M \in \powerset G: \map \phi M = M^\circ$
Then $\phi$ is a bijection.

Proof:
From Annihilator of Annihilator on Algebraic Dual of Subspace is Image under Evaluation Isomorphism, we have that:
:$M^{\circ \circ} = J \sqbrk M$
From Evaluation Isomorphism is Isomorphism, $J: G \to G^{**}$ is a bijection.
{{finish|I may return to this if I can view it once more with a clear head. It's not completely clear what's happening here.}}
Theorem: Inverse of Mapping to Annihilator on Algebraic Dual is Bijection

The inverse of $\phi$ is the bijection:
:$N \to \map {J^\gets} {N^\circ}$

Proof:
By definition::
:$\paren {\map {J^\gets} {N^\circ} }^\circ = \set {z \in G^*: \forall x \in G: \forall t \in N: \map t x = 0: \map z x = 0}$
Thus:
:$N \subseteq \paren {\map {J^\gets} {N^\circ} }^\circ$
But as $\paren {\map {J^\gets} {N^\circ} }^\circ$ has dimension $n - \paren {n - p} = p$, it follows that $N = \paren {\map {J^\gets} {N^\circ} }^\circ$ by Dimension of Proper Subspace is Less Than its Superspace.
This follows by the definition of an inverse mapping.
{{qed}}