avewright/proofwiki-math huggingface dataset:
Theorem: Set of Subfields forms Complete Lattice

Let $\struct {F, +, \circ}$ be a field.
Let $\mathbb F$ be the set of all subfields of $F$.
Then $\struct {\mathbb F, \subseteq}$ is a complete lattice.

Proof:
Let $\O \subset \mathbb S \subseteq \mathbb F$.
By Intersection of Subfields is Largest Subfield Contained in all Subfields:
:$\bigcap \mathbb S$ is the largest subfield of $F$ contained in each of the elements of $\mathbb S$.
By Intersection of Subfields Containing Subset is Smallest:
:The intersection of the set of all subfields of $F$ containing $\bigcup \mathbb S$ is the smallest subfield of $F$ containing $\bigcup \mathbb S$.
Thus:
:Not only is $\bigcap \mathbb S$ a lower bound of $\mathbb S$, but also the largest, and therefore an infimum.
:The supremum of $\mathbb S$ is the intersection of the set of all subfields of $R$.
Therefore $\struct {\mathbb F, \subseteq}$ is a complete lattice.
{{qed}}
Theorem: Properties of Prime Subfield

Let $F$ be a field.
Let $K$ be the prime subfield of $F$.
Then $K$ is isomorphic to either:
:$\Q$, the field of rational numbers, or
:$\Z_p$, the Ring of Integers Modulo $p$, where $p$ is prime.

Proof:
From Field of Characteristic Zero has Unique Prime Subfield, if $\Char F = 0$, then its prime subfield is isomorphic to $\Q$, the field of rational numbers.
From Field of Prime Characteristic has Unique Prime Subfield, if $\Char F = p$, then its prime subfield is isomorphic to $\Z_p$, the Ring of Integers Modulo $p$.
From Characteristic of Field is Zero or Prime, $p$ is prime.
{{Qed}}
Theorem: Subgroup of Additive Group Modulo m is Ideal of Ring

Let $m \in \Z: m > 1$.
Let $\struct {\Z_m, +_m}$ be the additive group of integers modulo $m$.
Then every subgroup of $\struct {\Z_m, +_m}$ is an ideal of the ring of integers modulo $m$ $\struct {\Z_m, +_m, \times_m}$.

Proof:
Let $H$ be a subgroup of $\struct {\Z_m, +_m}$
Suppose:
: $(1): \quad h + \ideal m \in H$, where $\ideal m$ is a principal ideal of $\struct {\Z_m, +_m, \times_m}$
and 
: $(2): \quad n \in \N_{>0}$.
Then by definition of multiplication on integers and Homomorphism of Powers as applied to integers:
{{begin-eqn}}
{{eqn | l = \paren {n + \ideal m} \times \paren {h + \ideal m}
      | r = \map {q_m} n \times \map {q_m} h
      | c = where $q_m$ is the quotient mapping
}}
{{eqn | r = \map {q_m} {n \times h}
      | c = 
}}
{{eqn | r = \map {q_m} {n \cdot h}
      | c = 
}}
{{eqn | r = n \cdot \map {q_m} h
      | c = 
}}
{{end-eqn}}
But:
:$n \cdot \map {q_m} h \in \gen {\map {q_m} h}$
where $\gen {\map {q_m} h}$ is the group generated by $\map {q_m} h$.
Hence by Epimorphism from Integers to Cyclic Group, $n \cdot \map {q_m} h \in H$.
The result follows.
{{qed}}
Theorem: Bijection from Divisors to Subgroups of Cyclic Group

Let $G$ be a cyclic group of order $n$ generated by $a$.
Let $S = \set {m \in \Z_{>0}: m \divides n}$ be the set of all divisors of $n$.
Let $T$ be the set of all subgroups of $G$
Let $\phi: S \to T$ be the mapping defined as:
:$\phi: m \to \gen {a^{n / m} }$
where $\gen {a^{n / m} }$ is the subgroup generated by $a^{n / m}$.
Then $\phi$ is a bijection.

Proof:
From Subgroup of Finite Cyclic Group is Determined by Order, there exists exactly one subgroup $\gen {a^{n / m} }$ of $G$ with $a$ elements.
So the mapping as defined is indeed a bijection by definition.
{{qed}}
Theorem: Generator of Additive Group Modulo m iff Unit of Ring

Let $m \in \Z: m > 1$.
Let $\struct {\Z_m, +_m}$ denote the additive group of integers modulo $m$.
Let $\struct {\Z_m, +_m, \times_m}$ be the ring of integers modulo $m$.
Let $a \in \Z_m$.
Then:
:$a$ is a generator of $\struct {\Z_m, +_m}$ 
{{iff}}
:$a$ is a unit of $\struct {\Z_m, +_m, \times_m}$

Proof:
From Integers under Addition form Infinite Cyclic Group, the identity element $1_\Z$ of the ring of integers $\struct {\Z, +, \times}$ is a generator of the group $\struct {\Z, +}$.
Thus from Quotient Group of Cyclic Group, the identity element $1_{\Z_m}$ of the ring $\struct {\Z_m, +_m, \times_m}$ is a generator of the group $\struct {\Z_m, +_m}$.
Let $a \in \Z_m$.
Suppose $1_{\Z_m} \in \gen a$, where $\gen a$ signifies the group generated by $a$.
Then the smallest subgroup of $\struct {\Z_m, +_m}$ containing $1_{\Z_m}$, that is $\struct {\Z_m, +_m}$ itself, is contained in $\gen a$.
Thus $\gen a = \struct {\Z_m, +_m}$ iff $1_{\Z_m} \in \gen a$.
However, from Subgroup of Additive Group Modulo m is Ideal of Ring, $\gen a$ is an ideal of $\struct {\Z_m, +_m, \times_m}$, and hence is the principal ideal $\ideal a$ generated by $a$.
But from Principal Ideal from Element in Center of Ring, $1_{\Z_m} \in \gen a$ {{iff}} $a$ is a unit of the ring $\struct {\Z_m, +_m, \times_m}$.
Hence the result.
{{qed}}
Theorem: Subspace of Real Differentiable Functions

Let $\mathbb J$ be an open interval of the real number line $\R$.
Let $\map \DD {\mathbb J}$ be the set of all differentiable real functions on $\mathbb J$.
Then $\struct {\map \DD {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.

Proof:
Note that by definition, $\map \DD {\mathbb J} \subseteq \R^{\mathbb J}$. 
Let $f, g \in \map \DD {\mathbb J}$. 
Let $\lambda \in \R$.
From Linear Combination of Derivatives, we have that: 
:$f + \lambda g$ is differentiable on $\mathbb J$. 
That is: 
:$f + \lambda g \in \map \DD {\mathbb J}$
So, by One-Step Vector Subspace Test:
:$\struct {\map \DD {\mathbb J}, +, \times}_\R$ is a subspace of $\R^{\mathbb J}$. 
{{qed}}
Theorem: Subspace of Real Functions of Differentiability Class

Let $\mathbb J = \set {x \in \R: a < x < b}$ be an open interval of the real number line $\R$.
Let $\map {C^m} {\mathbb J}$ be the set of all continuous real functions on $\mathbb J$ in differentiability class $m$.
Then $\struct {\map {C^m} {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.

Proof:
Note that by definition, $\map {C^m} {\mathbb J} \subseteq \R^{\mathbb J}$.
Let $f, g \in \map {C^m} {\mathbb J}$.
Let $\lambda \in \R$.
Applying Linear Combination of Derivatives $m$ times we have: 
:$f + \lambda g$ is $m$-times differentiable on $\mathbb J$ with $m$th derivative $f^{\paren m} + \lambda g^{\paren m}$.
Since both $f$ and $g$ are of differentiability class $m$:
:$f^{\paren m}$ and $g^{\paren m}$ are continuous on $\mathbb J$. 
From Combined Sum Rule for Continuous Real Functions:
:$f^{\paren m} + \lambda g^{\paren m} = \paren {f + \lambda g}^{\paren m}$ is continuous on $\mathbb J$.
So:
:$f + \lambda g \in \map {C^m} {\mathbb J}$
Therefore, by One-Step Vector Subspace Test:
:$\struct {\map {C^m} {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$.
{{qed}}
Theorem: Subspace of Riemann Integrable Functions

Let $\mathbb J = \set {x \in \R: a \le x \le b}$ be a closed interval of the real number line $\R$.
Let $\map \RR {\mathbb J}$ be the set of all Riemann integrable functions on $\mathbb J$.
Then $\struct {\map \RR {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.

Proof:
Note that by definition, $\map \RR {\mathbb J} \subseteq \R^{\mathbb J}$. 
Let $f, g \in \map \RR {\mathbb J}$.
Let $\lambda \in \R$.
By Linear Combination of Definite Integrals:
:$f + \lambda g$ is Riemann integrable on $\mathbb J$.
That is: 
:$f + \lambda g \in \map \RR {\mathbb J}$
So by One-Step Vector Subspace Test:
:$\struct {\map \RR {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$.
{{qed}}
Theorem: Basis of Vector Space of Polynomial Functions

Let $B$ be the set of all the identity functions $I^n$ on $\R^n$ where $n \in \N^*$.
Then $B$ is a basis of the $\R$-vector space $\map P \R$ of all polynomial functions on $\R$.

Proof:
By definition, every real polynomial function is a linear combination of $B$.
Suppose:
:$\ds \sum_{k \mathop = 0}^m \alpha_k I^k = 0, \alpha_m \ne 0$
Then by differentiating $m$ times, we obtain from Nth Derivative of Nth Power:
:$m! \alpha_m = 0$
whence $\alpha_m = 0$ which is a contradiction.
Hence $B$ is linearly independent and therefore is a basis for $\map P \R$.
{{qed}}
Theorem: Ordered Basis for Coordinate Plane

Let $a_1, a_2 \in \R^2$ such that $\set {a_1, a_2}$ forms a linearly independent set.
Then $\tuple {a_1, a_2}$ is an ordered basis for the $\R$-vector space $\R^2$.
Hence the points on the plane can be uniquely identified by means of linear combinations of $a_1$ and $a_2$.

Proof:
:500pxrightthumb
Let $P$ be any point in the plane for which we want to provide a linear combination of $a_1$ and $a_2$.
Let the distance from $O$ to the point determined by $a_1$ be defined as being $1$ unit of length on the line $L_1$.
Let the distance from $O$ to the point determined by $a_2$ be defined as being $1$ unit of length on the line $L_2$.
Draw lines parallel to $L_1$ and $L_2$ through $P$.
Then the coordinates $\lambda_1$ and $\lambda_2$ of $P$ are given by:
:$P = \lambda_1 a_1 + \lambda_2 a_2$
by the Parallelogram Law.
{{ProofWanted}}
Theorem: Differentiation on Polynomials is Linear Operator

Let $\map P \R$ be the vector space of all polynomial functions on the real number line $\R$.
Then the differentiation operator $D$ on $\map P \R$ is a linear operator.

Proof:
Let $\map f x, \map g x$ be real functions which are differentiable on $\R$.
Then from Linear Combination of Derivatives:
:$\forall x \in I: \map D {\lambda \map f x + \mu \map g x} = \lambda D \map f x + \mu D \map g x$
It follows from Real Polynomial Function is Differentiable that $\lambda D \map f x + \mu D \map g x$ is differentiable on $\R$.
The result follows from Condition for Linear Transformation.
{{qed}}
Theorem: Integration on Polynomials is Linear Operator

Let $\map P \R$ be the vector space of all polynomial functions on the real number line $\R$.
Let $S$ be the mapping defined as:
:$\ds \forall p \in \map P \R: \forall x \in \R: \map S {\map p x} = \int_0^x \map p t \rd t$
Then $S$ is a linear operator on $\map P \R$.

Proof:
Let $\map f x, \map g x$ be real functions which are integrable on $\R$.
Let $\closedint a b$ be a closed interval of $\R$.
Then from Linear Combination of Definite Integrals, $\lambda f + \mu g$ is integrable on $\closedint a b$ and:
:$\ds \int_a^b \paren {\lambda \map f t + \mu \map g t} \rd t = \lambda \int_a^b \map f t \rd t + \mu \int_a^b \map g t \rd t$
From Real Polynomial Function is Continuous:
:$\forall p \in \map P \R: p$ is continuous on $\R$.
From Continuous Real Function is Darboux Integrable:
:$\forall p \in \map P \R: p$ is integrable on $\R$.
The result follows from Condition for Linear Transformation.
{{qed}}
Theorem: Transpose of Linear Transformation is a Linear Transformation

Let $R$ be a commutative ring.
Let $G$ and $H$ be $R$-modules.
Let $G^*$ and $H^*$ be the algebraic duals of $G$ and $H$ respectively.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Let $u \in \map {\LL_R} {G, H}$.
Let $u^\intercal: H^* \to G^*$ be the transpose of $u$.
Then $u^\intercal: H^* \to G^*$ is itself a linear transformation.

Proof:
By definition of evaluation linear transformation:
:$\forall x \in G: y \in H^*: \innerprod x {\map {u^\intercal} y} = \innerprod {\map u x} y$
Since we have:
{{begin-eqn}}
{{eqn | l = \innerprod x {\map {u^\intercal} {y + z} }
      | r = \innerprod {\map u x} {y + z}
      | c = 
}}
{{eqn | r = \innerprod {\map u x} y + \innerprod {\map u x} z
      | c = 
}}
{{eqn | r = \innerprod x {\map {u^\intercal} y} + \innerprod x {\map {u^\intercal} z}
      | c = 
}}
{{eqn | r = \innerprod x {\map {u^\intercal} y + \map {u^\intercal} z}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \innerprod x {\map {u^\intercal} {\lambda y} }
      | r = \innerprod {\map u x} {\lambda y}
      | c = 
}}
{{eqn | r = \lambda \innerprod {\map u x} y
      | c = 
}}
{{eqn | r = \lambda \innerprod x {\map {u^\intercal} y}
      | c = 
}}
{{eqn | r = \innerprod x {\lambda \map {u^\intercal} y}
      | c = 
}}
{{end-eqn}}
it follows that $u^\intercal: H^* \to G^*$ is a linear transformation.
{{qed}}
Theorem: Equivalence of Definitions of Supremum of Real-Valued Function

Let $S \subseteq \R$ be a subset of the real numbers.
Let $f: S \to \R$ be a real function on $S$.
{{TFAE|def = Supremum of Real-Valued Function}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $K \in \R$ be a supremum of $f$ by definition 1.
Then from the definition:
:$\text{(a)}: \quad K$ is an upper bound of $\map f x$ in $\R$.
:$\text{(b)}: \quad K \le M$ for all upper bounds $M$ of $f \sqbrk S$ in $\R$.
As $K$ is an upper bound it follows that:
:$(1): \quad \forall x \in S: \map f x \le K$
Now let $\epsilon \in \R_{>0}$.
{{AimForCont}} $(2)$ were false:
:$\forall x \in S: \map f x \le K - \epsilon$
Then by definition, $K - \epsilon$ is an upper bound of $f$.
But by definition that means $K \le K + \epsilon$.
So by Real Plus Epsilon:
:$K < K$
From this contradiction we conclude that:
:$(2): \quad \exists x \in S: \forall \epsilon \in \R_{>0}: K - \epsilon < \map f x$
Thus $K$ is a supremum of $f$ by definition 2.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Infimum of Real-Valued Function

Let $S \subseteq \R$ be a subset of the real numbers.
Let $f: S \to \R$ be a real function on $S$.
{{TFAE|def = Infimum of Real-Valued Function}}

Proof:
{{wtd|Use Characterizing Property of Infimum of Subset of Real Numbers}}
Theorem: Supremum does not Precede Infimum

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ admit both a supremum $M$ and an infimum $m$.
Then $m \preceq M$.

Proof:
By definition of supremum:
:$\forall a \in T: a \preceq M$
By definition of infimum:
:$\forall a \in T: m \preceq a$
The result follows from transitivity of ordering.
{{qed}}
Theorem: Integer Multiples form Commutative Ring

Let $n \Z$ be the set of integer multiples of $n$.
Then $\struct {n \Z, +, \times}$ is a commutative ring.
Unless $n = 1$, $\struct {n \Z, +, \times}$ is not a ring with unity.

Proof:
From Integer Multiples under Addition form Infinite Cyclic Group, $\struct {n \Z, +}$ is a cyclic group
From Cyclic Group is Abelian, $\struct {n \Z, +}$ is abelian.
From Integer Multiples Closed under Multiplication and Integer Multiplication is Associative, we have that $\struct {n \Z, \times}$ is a semigroup.
From Integer Multiplication Distributes over Addition it follows that $\struct {n \Z, +, \times}$ is a ring.
From Integer Multiplication is Commutative we have that $\struct {n \Z, +, \times}$ is a commutative ring.
So $\struct {n \Z, +, \times}$ is a commutative ring.
{{qed|lemma}}
The unity of $\struct {\Z, +, \times}$ is $1$.
But unless $n = 1$, we have that $1 \notin n \Z$.
As $\struct {\Z, +, \times}$ is an integral domain, all its elements are cancellable, by the Cancellation Law for Ring Product of Integral Domain.
We have that Subrings of Integers are Sets of Integer Multiples.
From Identity of Cancellable Monoid is Identity of Submonoid it follows that $\struct {n \Z, +, \times}$ has no unity, because if it did, that unity would be $1$.
{{qed}}
Theorem: Matrix Form of Quaternion

Let $\mathbf x$ be a quaternion such that:
:$\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$
When the quaternion basis is expressed in the form of matrices:
:<nowiki>$\mathbf 1 = \begin{bmatrix} 1 & 0 \\ 0 & 1 \end{bmatrix}
\qquad
\mathbf i = \begin{bmatrix} i & 0 \\ 0 & -i \end{bmatrix}
\qquad
\mathbf j = \begin{bmatrix} 0 & 1 \\ -1 & 0 \end{bmatrix}
\qquad
\mathbf k = \begin{bmatrix} 0 & i \\ i & 0 \end{bmatrix}$</nowiki>
the general quaternion $\mathbf x$ has the form:
:$\mathbf x = \begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix}$
or:
:$\mathbf x = \begin{bmatrix} w & z \\ -\overline z & \overline w \end{bmatrix}$
where :
:$w$ and $z$ are complex numbers
:$\overline z$ is the complex conjugate of $z$.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf x
      | r = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k
      | c = 
}}
{{eqn | r = a \begin{bmatrix} 1 & 0 \\ 0 & 1 \end{bmatrix} + b \begin{bmatrix} i & 0 \\ 0 & -i \end{bmatrix} + c \begin{bmatrix} 0 & 1 \\ -1 & 0 \end{bmatrix} + d \begin{bmatrix} 0 & i \\ i & 0 \end{bmatrix}
      | c = 
}}
{{eqn | r = \begin{bmatrix} a & 0 \\ 0 & a \end{bmatrix} + \begin{bmatrix} b i & 0 \\ 0 & - b i \end{bmatrix} + \begin{bmatrix} 0 & c \\ -c & 0 \end{bmatrix} + \begin{bmatrix} 0 & d i \\ d i & 0 \end{bmatrix}
      | c = 
}}
{{eqn | r = \begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Quaternion Multiplication

Let $\mathbf x_1 = a_1 \mathbf 1 + b_1 \mathbf i + c_1 \mathbf j + d_1 \mathbf k$ and $\mathbf x_2 = a_2 \mathbf 1 + b_2 \mathbf i + c_2 \mathbf j + d_2 \mathbf k$ be quaternions.
Then their '''product''' is given by:
{{begin-eqn}}
{{eqn | ll=\mathbf x_1 \mathbf x_2
      | l==
      | o=
      | r=\left({a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2}\right) \mathbf 1
      | c=
}}
{{eqn | o=+
      | r=\left({a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2}\right) \mathbf i
      | c=
}}
{{eqn | o=+
      | r=\left({a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2}\right) \mathbf j
      | c=
}}
{{eqn | o=+
      | r=\left({a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2}\right) \mathbf k
      | c=
}}
{{end-eqn}}

Proof:
From Matrix Form of Quaternion we have that:
:$\mathbf x_1 \mathbf x_2 = \begin{bmatrix} a_1 + b_1 i & c_1 + d_1 i \\ -c_1 + d_1 i & a_1 - b_1 i \end{bmatrix} \begin{bmatrix} a_2 + b_2 i & c_2 + d_2 i \\ -c_2 + d_2 i & a_2 - b_2 i \end{bmatrix}$
Let $\mathbf x_1 \mathbf x_2 = \begin{bmatrix} p_{11} & p_{12} \\ p_{21} & p_{22} \end{bmatrix} = \begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix}$.
Throughout we use the definition of conventional matrix product.
So:
{{begin-eqn}}
{{eqn | l=p_{11}
      | r=\left({a_1 + b_1 i}\right) \left({a_2 + b_2 i}\right) + \left({c_1 + d_1 i}\right) \left({-c_2 + d_2 i}\right)
      | c=
}}
{{eqn | r=a_1 a_2 + b_1 a_2 i + a_1 b_2 i + b_1 b_2 i^2 - c_1 c_2 - d_1 c_2 i + c_1 d_2 i + d_1 d_2 i^2
      | c=
}}
{{eqn | r=\left({a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2}\right) + \left({a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2}\right) i
      | c=
}}
{{eqn | r=a + b i
      | c=
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l=p_{12}
      | r=\left({a_1 + b_1 i}\right) \left({c_2 + d_2 i}\right) + \left({c_1 + d_1 i}\right) \left({a_2 - b_2 i}\right)
      | c=
}}
{{eqn | r=a_1 c_2 + b_1 c_2 i + a_1 d_2 i + b_1 d_2 i^2 + c_1 a_2 + d_1 a_2 i - c_1 b_2 i - d_1 b_2 i^2
      | c=
}}
{{eqn | r=\left({a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2}\right) + \left({a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2}\right) i
      | c=
}}
{{eqn | r=c + d i
      | c=
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l=p_{21}
      | r=\left({-c_1 + d_1 i}\right) \left({a_2 + b_2 i}\right) + \left({a_1 - b_1 i}\right) \left({-c_2 + d_2 i}\right)
      | c=
}}
{{eqn | r=-c_1 a_2 + d_1 a_2 i - c_1 b_2 i + d_1 b_2 i^2 - a_1 c_2 + b_1 c_2 i + a_1 d_2 i - b_1 d_2 i^2
      | c=
}}
{{eqn | r=-\left({a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2}\right) + \left({a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2}\right) i
      | c=
}}
{{eqn | r=-c + d i
      | c=
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l=p_{22}
      | r=\left({-c_1 + d_1 i}\right) \left({c_2 + d_2 i}\right) + \left({a_1 - b_1 i}\right) \left({a_2 - b_2 i}\right)
      | c=
}}
{{eqn | r=-c_1 c_2 + d_1 c_2 i - c_1 d_2 i + d_1 d_2 i^2 + a_1 a_2 - b_1 a_2 i - a_1 b_2 i + b_1 b_2 i^2
      | c=
}}
{{eqn | r=\left({a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2}\right) - \left({a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2}\right) i
      | c=
}}
{{eqn | r=a - b i
      | c=
}}
{{end-eqn}}
Hence the result from Matrix Form of Quaternion.
{{qed}}
Category:Quaternions
5ppc4f8h3le29g9xdsoky7nc4e6u7im
Theorem: Quaternion Addition forms Abelian Group

Let $\mathbb H$ be the set of quaternions.
Then $\struct {\mathbb H, +}$, where $+$ denotes quaternion addition, is an abelian group.

Proof:
Taking the abelian group axioms in turn:
Theorem: Ring of Quaternions is Ring

The set $\mathbb H$ of quaternions forms a ring under the operations of addition and multiplication.

Proof:
From Quaternion Addition forms Abelian Group, $\mathbb H$ forms an abelian group under quaternion addition.
From the definition it is clear that quaternion multiplication is closed.
We have from Matrix Form of Quaternion that quaternions can be expressed in matrix form.
From Quaternion Multiplication we have that quaternion multiplication can be expressed in terms of matrix multiplication, which is associative.
So $\mathbb H$ forms a semigroup under quaternion multiplication.
Finally, we have that Matrix Multiplication Distributes over Matrix Addition.
So all the conditions are fulfilled for $\mathbb H$ to be a ring.
{{qed}}
Theorem: Quaternions Subring of Complex Matrix Space

The Ring of Quaternions is a subring of the matrix space $\map {\MM_\C} 2$.

Proof:
From Matrix Form of Quaternion it is clear that the quaternions $\H$ can be expressed in matrix form, as elements of $\map {\MM_\C} 2$.
Thus $\H \subseteq \map {\MM_\C} 2$.
As the quaternions form a ring, the result follows by definition of subring.
{{qed}}
Theorem: Product of Quaternion with Conjugate

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion.
Let $\overline {\mathbf x}$ be the conjugate of $\mathbf x$.
Then their product is given by:
:$\mathbf x \overline {\mathbf x} = \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1 = \overline {\mathbf x} \mathbf x$

Proof:
From the definition of quaternion multiplication:
{{begin-eqn}}
{{eqn | l = \mathbf x \overline {\mathbf x}
      | r = \paren {a^2 - b \paren {-b} - c \paren {-c} - d \paren {-d} } \mathbf 1
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {a \paren {-b} + b a + c \paren {-d} - d \paren {-c} } \mathbf i
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {a \paren {-c} - b \paren {-d} + c a + d \paren {-b} } \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {a \paren {-d} + b \paren {-c} - c \paren {-b} + d a} \mathbf k
      | c = 
}}
{{eqn | r = \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {-a b + b a - c d + d c} \mathbf i
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {-a c + b d + c a - d b} \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {-a d - b c + c b + d a} \mathbf k
      | c = 
}}
{{end-eqn}}
We have that $a, b, c, d \in \R$.
So from Real Multiplication is Commutative, their products commute.
So the terms in $\mathbf i, \mathbf j, \mathbf k$ vanish.
The proof that $\overline {\mathbf x} \mathbf x = \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1$ is similar.
Hence the result.
{{qed}}
Theorem: Multiplicative Inverse of Quaternion

Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion such that $\mathbf x \ne \mathbf 0$.
Then $\mathbf x$ has an inverse $\mathbf x^{-1}$ under the operation of quaternion multiplication:
:$\mathbf x^{-1} = \lambda \overline {\mathbf x}$
where:
:$\lambda = \dfrac 1 {a^2 + b^2 + c^2 + d^2} \mathbf 1$

Proof:
From Multiplicative Identity for Quaternions, we need to show that $\lambda \overline{\mathbf x} \mathbf x = \mathbf 1 = \mathbf x \lambda \overline{\mathbf x}$.
From Product of Quaternion with Conjugate we have that:
:$\overline{\mathbf x} \mathbf x = \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1$
Using the definition of $\lambda$ from above:
{{begin-eqn}}
{{eqn | l = \lambda \overline{\mathbf x} \mathbf x
      | r = \paren {\frac 1 {a^2 + b^2 + c^2 + d^2} } \mathbf 1 \paren {a^2 + b^2 + c^2 + d^2} \mathbf 1
      | c = 
}}
{{eqn | r = \paren {\frac {a^2 + b^2 + c^2 + d^2} {a^2 + b^2 + c^2 + d^2} } \mathbf 1
      | c = {{Defof|Quaternion Multiplication}}
}}
{{eqn | r = \mathbf 1
      | c = 
}}
{{end-eqn}}
Unless all of $a, b, c, d = 0$ we have that $a^2 + b^2 + c^2 + d^2 \ne 0$.
Therefore $\lambda$ is defined for all quaternions not equal to $\mathbf 0$.
It follows from Left Inverse for All is Right Inverse that $\mathbf x \lambda \overline{\mathbf x} = \mathbf 1$.
Hence the result.
{{qed}}