avewright/proofwiki-math huggingface dataset:
Theorem: Union of Upper Sections is Upper

Let $\struct {S, \preceq}$ be a preordered set.
Let $A$ be a set of subsets of $S$ such that:
:$\forall X \in A: X$ is an upper section.
Then:
:$\bigcup A$ is also an upper section.

Proof:
Let $x \in \bigcup A, y \in S$ such that:
:$x \preceq y$
By definition of union:
:$\exists Y \in A: x \in Y$
By assumption:
:$Y$ is an upper section.
By definition of upper section:
:$y \in Y$
Thus by definition of union:
:$y \in \bigcup A$
Hence
:$\bigcup A$ is an upper section.
{{qed}}
Theorem: Set of Rotations in Space about Fixed Point forms Infinite Group

Let $\SS$ be a rigid body in space.
Let $O$ be a fixed point in space.
The set of all rotations of $\SS$ through some straight line through $O$ forms an infinite group.

Proof:
{{ProofWanted|Needs the mathematical definition of a rotation in space to be defined before we start.}}
Theorem: Group of Rotations about Fixed Point is not Abelian

Let $\SS$ be a rigid body in space.
Let $O$ be a fixed point in space.
Let $\GG$ be the group of all rotations of $\SS$ around $O$.
Then $\GG$ is not an abelian group.

Proof:
Let $\SS$ be a square lamina.
Let $O$ be the center of $\SS$.
Recall the definition of the symmetry group of the square $D_4$:
{{:Definition:Symmetry Group of Square}}
We have that:
:Reflection $t_x$ can be achieved by a rotation of $\SS$ of $\pi$ radians about $x$.
:Reflection $t_y$ can be achieved by a rotation of $\SS$ of $\pi$ radians about $y$.
Thus $D_4$ forms a subgroup of $\GG$.
From Symmetry Group of Square is Group we have that $D_4$ is not abelian.
From Subgroup of Abelian Group is Abelian it follows that $\GG$ is also not abelian.
{{qed}}
Theorem: Union of Filtered Sets is Filtered

Let $\struct {S, \preceq}$ be a preordered set.
Let $A$ be a set of subsets of $S$ such that
:$\forall X \in A: X$ is filtered
and
:$\forall X, Y \in A: \exists Z \in A: X \cup Y \subseteq Z$
Then:
:$\bigcup A$ is also filtered.

Proof:
Let $x, y \in \bigcup A$.
By definition of union:
:$\exists X \in A: x \in X$
and
:$\exists Y \in A: y \in Y$
By assumption:
:$\exists Z \in A: X \cup Y \subseteq Z$
By definition of union:
:$x, y \in X \cup Y$
By definition of subset:
:$x, y \in Z$
By assumption:
:$Z$ is filtered.
By definition of filtered:
:$\exists z \in Z: z \preceq x \land z \preceq y$
Thus by definition of union:
:$z \in \bigcup A$
Hence
:$\bigcup A$ is filtered.
{{qed}}
Theorem: Special Orthogonal Group is Group

Let $k$ be a field.
The $n$th orthogonal group on $k$ is a group.

Proof:
A direct corollary of Special Orthogonal Group is Subgroup of Orthogonal Group.
{{qed}}
Theorem: Unit Matrix is its own Inverse

The inverse of the unit matrix $\mathbf I_n$ of order $n$ is $\mathbf I_n$.
That is, a unit matrix it its own inverse.

Proof:
By definition, a unit matrix is a diagonal matrix.
From Inverse of Diagonal Matrix, the inverse of a diagonal matrix:
:<nowiki>$\mathbf D = \begin{bmatrix}
a_{11} & 0 & \cdots & 0 \\
0 & a_{22} & \cdots & 0 \\
\vdots & \vdots & \ddots & \vdots \\
0 & 0 & \cdots & a_{nn} \\
\end{bmatrix}$</nowiki>
is the diagonal matrix:
:<nowiki>$\mathbf D^{-1} = \begin{bmatrix}
\dfrac 1 {a_{11}} & 0 & \cdots & 0 \\
0 & \dfrac 1 {a_{22}} & \cdots & 0 \\
\vdots & \vdots & \ddots & \vdots \\
0 & 0 & \cdots & \dfrac 1 {a_{nn}} \\
\end{bmatrix}$</nowiki>
When $\mathbf D$ is the unit matrix $\mathbf I_n$, all elements $a_{kk}$ are equal to $1$:
:<nowiki>$\mathbf I_n = \begin{bmatrix}
1 & 0 & \cdots & 0 \\
0 & 1 & \cdots & 0 \\
\vdots & \vdots & \ddots & \vdots \\
0 & 0 & \cdots & 1 \\
\end{bmatrix}$</nowiki>
Hence:
:<nowiki>$\mathbf I_n^{-1} = \begin{bmatrix}
\dfrac 1 1 & 0 & \cdots & 0 \\
0 & \dfrac 1 1 & \cdots & 0 \\
\vdots & \vdots & \ddots & \vdots \\
0 & 0 & \cdots & \dfrac 1 1 \\
\end{bmatrix}$</nowiki>
Hence the result.
{{qed}}
Category:Unit Matrices
Category:Inverse Matrices
5tmtdw12m2ujo89gkp25x2i5g6d9pta
Theorem: Way Above Closure is Subset of Upper Closure of Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then:
:$x^\gg \subseteq x^\succeq$
where
:$x^\gg$ denotes the way above closure of $x$
:$x^\succeq$ denotes the upper closure of $x$.

Proof:
Let $y \in x^\gg$.
By definition of way above closure:
:$x \ll y$
where $\ll$ denotes the way below relation.
By Way Below implies Preceding:
:$x \preceq y$
Thus by definition of upper closure of element:
:$y \in x^\succeq$
{{qed}}
Theorem: Diagonal Matrix is Symmetric

Let $D$ be a diagonal matrix.
Then $D$ is symmetric.

Proof:
By definition of diagonal matrix:
:$\forall j, k: j \ne k \implies a_{jk} = 0 = a_{kj}$
So by definition of transpose of $D$:
:$D = D^\intercal$
where $D^\intercal$ denotes the transpose.
Hence the result, by definition of symmetric matrix.
{{qed}}
Category:Symmetric Matrices
Category:Diagonal Matrices
dv7n9kzvzryg6tjumxlrly9jp6semgo
Theorem: Unit Matrix is Orthogonal

The unit matrix $\mathbf I_n$ of order $n$ is orthogonal.

Proof:
By Unit Matrix is its own Inverse the inverse $I_n^{-1}$ of $I_n$ is $I_n$.
By definition a unit matrix is a diagonal matrix.
Hence by Diagonal Matrix is Symmetric:
:$I_n = I_n^\intercal$
where $I_n^\intercal$ is the transpose of $I_n$.
Thus:
:$I_n^{-1} = I_n^\intercal$
and the result follows by definition of orthogonal.
{{qed}}
Category:Unit Matrices
Category:Orthogonal Matrices
thfuv0wq4j5hsyxq6htlcafz1z4aotx
Theorem: Unit Matrix is Proper Orthogonal

The unit matrix $\mathbf I_n$ of order $n$ is proper orthogonal.

Proof:
By Unit Matrix is Orthogonal, $\mathbf I_n$ is an orthogonal matrix.
By Determinant of Unit Matrix, the determinant of $\mathbf I_n$ is equal to $1$.
The result follows by definition of proper orthogonal.
{{qed}}
Category:Unit Matrices
Category:Proper Orthogonal Matrices
3xdpyj4v5c1djkul1buy2fq721ardd4
Theorem: Inverse of Orthogonal Matrix is Orthogonal

Let $\mathbf A$ be an orthogonal matrix.
Then its inverse $\mathbf A^{-1}$ is also orthogonal.

Proof:
By definition of orthogonal matrix:
:$\mathbf A^\intercal = \mathbf A^{-1}$
where $\mathbf A^\intercal$ is the transpose of $\mathbf A$.
By Inverse of Inverse of Matrix:
:$\paren {\mathbf A^{-1} }^{-1} = \mathbf A$
By Transpose of Transpose of Matrix:
:$\paren {\mathbf A^\intercal}^\intercal = \mathbf A$
Thus we have:
:$\paren {\mathbf A^{-1} }^{-1} = \mathbf A = \paren {\mathbf A^\intercal}^\intercal = \paren {\mathbf A^{-1} }^\intercal$
and so by definition $\mathbf A^{-1}$ is orthogonal.
{{qed}}
Category:Orthogonal Matrices
Category:Inverse Matrices
8qgfo01t3z6dht0dvrmkf741k1527ht
Theorem: Inverse of Inverse of Matrix

Let $\mathbf A$ be a nonsingular matrix.
Then:
:$\paren {\mathbf A^{-1} }^{-1} = \mathbf A$
That is, a nonsingular matrix equals the inverse of its inverse.

Proof:
By definition of inverse matrix:
:$\mathbf A^{-1} \mathbf A = \mathbf I$
where $\mathbf I$ is the unit matrix.
Thus the inverse of $\mathbf A^{-1}$ is $\mathbf A$.
Hence the result.
{{qed}}
Category:Inverse Matrices
9l2e2amuqajjgd2tbsewqgpmsc67u4p
Theorem: Inverse of Proper Orthogonal Matrix is Proper Orthogonal

Let $\mathbf A$ be a proper orthogonal matrix.
Then its inverse $\mathbf A^{-1}$ is also proper orthogonal.

Proof:
By definition of proper orthogonal matrix:
:$\mathbf A$ is orthogonal
:the determinant of $\mathbf A$ is equal to $1$.
By Inverse of Orthogonal Matrix is Orthogonal, $\mathbf A^{-1}$ is orthogonal.
By Determinant of Inverse Matrix:
:$\det \mathbf A^{-1} = \dfrac 1 {\det \mathbf A} = 1$
Hence, by definition, $\mathbf A^{-1}$ is proper orthogonal.
{{qed}}
Category:Proper Orthogonal Matrices
Category:Inverse Matrices
tet43w10d2xqm9nyznrp2xap8l5ft31
Theorem: Special Orthogonal Group is Subgroup of Orthogonal Group

Let $k$ be a field.
Let $\map {\operatorname O} {n, k}$ be the $n$th orthogonal group on $k$.
Let $\map {\operatorname {SO} } {n, k}$ be the $n$th special orthogonal group on $k$.
Then $\map {\operatorname {SO} } {n, k}$ is a subgroup of $\map {\operatorname O} {n, k}$.

Proof:
We have that Unit Matrix is Proper Orthogonal, so $\map {\operatorname {SO} } {n, k}$ is not empty.
Let $\mathbf A, \mathbf B \in \map {\operatorname {SO} } {n, k}$.
Then, by definition, $\mathbf A$ and $\mathbf B$ are proper orthogonal.
Then by Inverse of Proper Orthogonal Matrix is Proper Orthogonal:
:$\mathbf B^{-1}$ is a proper orthogonal matrix.
By Product of Proper Orthogonal Matrices is Proper Orthogonal Matrix:
:$\mathbf A \mathbf B^{-1}$ is a proper orthogonal matrix.
Thus by definition of special orthogonal group:
:$\mathbf A \mathbf B^{-1} \in \map {\operatorname {SO} } {n, k}$
Hence the result by One-Step Subgroup Test.
{{qed}}
Category:Orthogonal Groups
c84yl527lbmgzjz3uiuiri8mcwzpl8t
Theorem: Negative Matrix is Inverse for Hadamard Product

Let $\struct {G, \cdot}$ be a group whose identity is $e$.
Let $\map {\MM_G} {m, n}$ be a $m \times n$ matrix space over $\struct {G, \cdot}$.
Let $\mathbf A$ be an element of $\map {\MM_G} {m, n}$.
Let $-\mathbf A$ be the negative of $\mathbf A$.
Then $-\mathbf A$ is the inverse for the operation $\circ$, where $\circ$ is the Hadamard product.

Proof:
Let $\mathbf A = \sqbrk a_{m n} \in \map {\MM_G} {m, n}$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A \circ \paren {-\mathbf A}
      | r = \sqbrk a_{m n} \circ \paren {-\sqbrk a_{m n} }
      | c = Definition of $\mathbf A$
}}
{{eqn | r = \sqbrk a_{m n} \circ \sqbrk {a^{-1} }_{m n}
      | c = {{Defof|Negative Matrix|subdef = General Group}}
}}
{{eqn | r = \sqbrk {a \cdot \paren {a^{-1} } }_{m n}
      | c = {{Defof|Hadamard Product}}
}}
{{eqn | r = \sqbrk e_{m n}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = \mathbf A \circ \paren {-\mathbf A}
      | r = \mathbf e
      | c = {{Defof|Zero Matrix over General Monoid}}
}}
{{end-eqn}}
The result follows from Zero Matrix is Identity for Hadamard Product.
{{qed}}
Theorem: Cancellable Infinite Semigroup is not necessarily Group

Let $\struct {S, \circ}$ be a semigroup whose underlying set is infinite.
Let $\struct {S, \circ}$ be such that all elements of $S$ are cancellable.
Then it is not necessarily the case that $\struct {S, \circ}$ is a group.

Proof:
Consider the semigroup $\struct {\N, +}$.
From Natural Numbers under Addition form Commutative Semigroup, $\struct {\N, +}$ forms a semigroup.
From Natural Numbers are Infinite, the underlying set of $\struct {\N, +}$ is infinite.
From Natural Number Addition is Cancellable, all elements of $\struct {\N, +}$ are cancellable.
But from Natural Numbers under Addition do not form Group, $\struct {\N, +}$ is not a group.
Theorem: Left Regular Representation wrt Left Cancellable Element on Finite Semigroup is Bijection

Let $\struct {S, \circ}$ be a finite semigroup.
Let $a \in S$ be left cancellable.
Then the left regular representation $\lambda_a$ of $\struct {S, \circ}$ with respect to $a$ is a bijection.

Proof:
By Left Cancellable iff Left Regular Representation Injective, $\lambda_a$ is an injection.
By hypothesis, $S$ is finite.
From Injection from Finite Set to Itself is Surjection, $\lambda_a$ is a surjection.
Thus $\lambda_a$ is injective and surjective, and therefore a bijection.
{{qed}}
Theorem: Right Regular Representation wrt Right Cancellable Element on Finite Semigroup is Bijection

Let $\struct {S, \circ}$ be a finite semigroup.
Let $a \in S$ be right cancellable.
Then the right regular representation $\rho_a$ of $\struct {S, \circ}$ with respect to $a$ is a bijection.

Proof:
By Right Cancellable iff Right Regular Representation Injective, $\rho_a$ is an injection.
By hypothesis, $S$ is finite.
From Injection from Finite Set to Itself is Surjection, $\rho_a$ is a surjection.
Thus $\rho_a$ is injective and surjective, and therefore a bijection.
{{qed}}
Theorem: Singleton is Chain

Let $\struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then $\set x$ is a chain of $\struct {S, \preceq}$.

Proof:
It suffices to prove that
:$\set x$ is connected
Let $y, z \in \set x$.
By definition of singleton:
:$y = x$ and $z = x$
By definition of reflexivity;
:$y \preceq z$
Thus
:$y \preceq z$ or $z \preceq y$
{{qed}}
Theorem: Identity Elements occupy Diagonal of Cayley Table in Inverse Row Form

Let $\struct {G, \circ}$ be a finite group.
Let $\CC$ be a Cayley table for $\struct {G, \circ}$ presented in inverse row form.
Then all the entries in the main diagonal of $\CC$
are instances of the identity element.

Proof:
By definition of inverse row form, the rows of $\CC$ are headed by the inverse elements of the elements which head the corresponding columns.
The entries in the main diagonal of $\CC$ have the same column number as row number.
Let $\sqbrk c_{k k}$ denote the entry of $\CC$ corresponding to the element where the $k$th row intersects the $k$th column.
Let $a$ be the element which heads column $k$.
Then, by definition, $a^{-1}$ is the element which heads row $k$.
Thus the element which occupies entry $\struct c_{k k}$ is $a^{-1} \circ a = e$.
Hence the result.
{{qed}}
Theorem: Latin Square is not necessarily Cayley Table of Group

While it is true that the Cayley table of a (finite) group is in the form of a Latin square it is not necessarily the case that a Latin square is the Cayley table of a group.

Proof:
Proof by Counterexample:
Let $\struct {S, \circ}$ be the algebraic structure defined by the following Cayley table:
:$\begin{array}{c|ccccc}
\circ & e & a & b & c & d \\
\hline
e & e & a & b & c & d  \\
a & a & e & d & b & c  \\
b & b & c & e & d & a  \\
c & c & d & a & e & b  \\
d & d & b & c & a & e  \\
\end{array}$
By inspection it can be seen that the Cayley table for $\struct {S, \circ}$ is a Latin square.
However, we have that:
:$\paren {a \circ b} \circ c = d \circ c = a$
:$a \circ \paren {b \circ c} = a \circ d = c$
Thus $\circ$ is not an associative operation.
So, by definition, $\struct {S, \circ}$ is not a group.
{{qed}}
Theorem: Scaling preserves Modulo Addition

Let $m \in \Z_{> 0}$.
Let $x, y, c \in \Z$.
Let $x \equiv y \pmod m$.
Then:
:$c x \equiv c y \pmod m$

Proof:
Let $x \equiv y \pmod m$.
Then by definition of congruence:
:$\exists k \in Z: x - y = k m$
Hence:
:$c x - c y = c k m$
and so by definition of congruence:
:$c x \equiv c y \pmod m$
{{qed}}
Category:Modulo Addition
5ro93s15864yankv4wl8fdte2utm0ix
Theorem: Modulo Addition is Linear

Let $m \in \Z_{> 0}$.
Let $x_1, x_2, y_1, y_2, c_1, c_2 \in \Z$.
Let:
:$x_1 \equiv y_1 \pmod m$
:$x_2 \equiv y_2 \pmod m$
Then:
:$c_1 x_1 + c_2 x_2 \equiv c_1 y_1 + c_2 y_2 \pmod m$

Proof:
By Scaling preserves Modulo Addition:
:$c_1 x_1 \equiv c_1 y_1 \pmod m$
:$c_2 x_2 \equiv c_2 y_2 \pmod m$
and so by Modulo Addition is Well-Defined:
:$c_1 x_1 + c_2 x_2 \equiv c_1 y_1 + c_2 y_2 \pmod m$
{{qed}}
Theorem: Euler Phi Function of Prime

Let $p$ be a prime number.
Then:
:$\map \phi p = p - 1$
where $\phi: \Z_{>0} \to \Z_{>0}$ is the Euler $\phi$ function.

Proof:
From the definition of a prime number, the only (strictly) positive integer less than or equal to a prime $p$ which is ''not'' prime to $p$ is $p$ itself.
Thus it follows directly that:
:$\map \phi p = p - 1$
{{qed}}
Theorem: Chain is Directed

Let $\struct {S, \preceq}$ be an ordered set.
Let $C$ be a non-empty chain of $S$.
Then $C$ is directed.

Proof:
Let $x, y \in C$.
By definition of connected relation:
:$x \preceq y$ or $y \preceq x$
{{WLOG}}, suppose that
:$x \preceq y$
Define $z = y$.
Thus by definition of reflexivity
:$x \preceq z$ and $y \preceq z$
Hence $C$ is directed.
{{qed}}
Theorem: Reduced Residue System Modulo Prime

Let $p$ be a prime number.
The reduced residue system modulo $p$ contains $p - 1$ elements:
:$Z'_p = \set {\eqclass 1 m, \eqclass 2 m, \ldots, \eqclass {p - 1} m}$
and so can be defined as:
:$Z'_p = Z_p \setminus \set {\eqclass 0 m}$

Proof:
From Prime not Divisor implies Coprime, each of $1, 2, \ldots, p - 1$ is coprime to $p$.
The result follows by definition of reduced residue system modulo $p$.
{{qed}}
Theorem: Modulo Multiplication on Reduced Residue System is Closed

Let $m \in \Z_{> 0}$ be a (strictly) positive integer.
Let $\Z'_m$ be the reduced residue system modulo $m$:
:$\Z'_m = \set {\eqclass k m \in \Z_m: k \perp m}$
Let $S = \struct {\Z'_m, \times_m}$ be the algebraic structure consisting of $\Z'_m$ under the modulo multiplication.
Then $S$ is closed, in the sense that:
:$\forall a, b \in \Z'_m: a \times_m b \in \Z'_m$

Proof:
Let $\eqclass r m, \eqclass s m \in \Z'_m$.
Then by definition of reduced residue system:
:$r, s \perp m$
By Bézout's Identity:
:$\exists u_1, v_1 \in \Z: u_1 r + v_1 m = 1$
:$\exists u_2, v_2 \in \Z: u_2 s + v_2 m = 1$
Then:
{{begin-eqn}}
{{eqn | l = \paren {u_1 r + v_1 m} \paren {u_2 s + v_2 m}
      | r = u_1 u_2 r s + v_1 u_2 s m + u_1 v_2 r m + v_1 v_2 m^2
      | c = 
}}
{{eqn | r = \paren {u_1 u_2} r s + \paren {v_1 u_2 s + u_1 v_2 r + v_1 v_2 m} m
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
So, again by Bézout's Identity, $r s$ is coprime to $m$.
So the product of two elements of $\struct {\Z'_m, \times_m}$ is again in $\struct {\Z'_m, \times_m}$.
That is, $\struct {\Z'_m, \times_m}$ is closed.
{{qed}}
Theorem: Modulo Multiplication on Reduced Residue System is Cancellable

Let $m \in \Z_{> 0}$ be a (strictly) positive integer.
Let $\Z'_m$ be the reduced residue system modulo $m$:
:$\Z'_m = \set {\eqclass k m \in \Z_m: k \perp m}$
Let $S = \struct {\Z'_m, \times_m}$ be the algebraic structure consisting of $\Z'_m$ under modulo multiplication.
Then $\times_m$ is cancellable, in the sense that:
:$\forall a, b, c \in \Z'_m: a \times_m c = b \times_m c \implies a = b$
and:
:$\forall a, b, c \in \Z'_m: c \times_m a = c \times_m b \implies a = b$

Proof:
Let $a, b, c \in \Z'_m$ such that $a \times_m c = b \times_m c$
Let $p, q, r$ be integers such that:
:$p \in a$
:$q \in b$
:$r \in c$
By definition of residue class, this means:
{{begin-eqn}}
{{eqn | l = p r
      | o = \equiv
      | r = q r
      | rr= \pmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p
      | o = \equiv
      | r = q
      | rr= \pmod m
      | c = Cancellability of Congruences: Corollary 1
}}
{{end-eqn}}
Thus as $p \in a$ and $q \in b$ it follows that $a = b$.
Hence the result.
{{qed}}
Theorem: Order Generating iff Every Element is Infimum

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
{{iff}}
:$\forall x \in S: \exists Y \subseteq X: x = \inf Y$

Proof:
=== Sufficient Condition ===
Let $X$ be order generating.
Let $x \in S$.
By definition of order generating:
:$x = \map \inf {x^\succeq \cap X}$
Thus
:$\exists Y \subseteq X: x = \inf Y$
{{qed|lemma}}
Theorem: Weierstrass Factorization Theorem

Let $f$ be an entire function.
Let $0$ be a zero of $f$ of multiplicity $m \ge 0$.
Let the sequence $\sequence {a_n}$ consist of the nonzero zeroes of $f$, repeated according to multiplicity.

Proof:
From Weierstrass Product Theorem, the function:
:$\ds \map h z = z^m \prod_{n \mathop = 1}^\infty \map {E_{p_n} } {\frac z {a_n} }$
defines an entire function that has the same zeroes as $f$ counting multiplicity. 
Thus $f / h$ is both an entire function and non-vanishing.
As $f / h$ is both holomorphic and nowhere zero there exists a holomorphic function $g$ such that:
:$e^g = f / h$
Therefore:
:$f = e^g h$
as desired.
{{qed}}
Theorem: Equivalence of Axiom Schemata for Finite Group

The following axiom schemata for the definition of a finite group are logically equivalent:

Proof:
Let $S$ be an algebraic structure of finite order which fulfils the group axioms.
It is to be shown that $S$ also fulfils all the finite group axioms.
We have that $\text {FG} 0$ and $\text {FG} 1$ are the same as $\text G 0$ and $\text G 1$ and so {{apriori}} $\text {FG} 0$ and $\text {FG} 1$ are fulfilled.
We also have that {{hypothesis}} $S$ is of finite order.
That is, there exists some (strictly) positive integer $n$ such that $s$ has exactly $n$ elements.
That is, $\text {FG} 2$ is fulfilled.
As $S$ fulfils the group axioms, it is by definition a group.
Therefore the Cancellation Laws hold:
:$b a = c a \implies b = c$
:$a b = a c \implies b = c$
That is, $\text {FG} 3$ is fulfilled.
Thus, $S$ fulfils all the finite group axioms.
{{qed|lemma}}
Let $S$ be an algebraic structure which fulfils the finite group axioms.
It is to be shown that $S$ also fulfils all the group axioms.
We have that $\text G 0$ and $\text G 1$ are the same as $\text {FG} 0$ and $\text {FG} 1$ and so {{apriori}} $\text G 0$ and $\text G 1$ are fulfilled.
By definition, an algebraic structure which fulfils group axioms $\text G 0$ and $\text G 1$ is a semigroup.
From Cancellable Finite Semigroup is Group, it then follows that $S$ is a group.
That is, $S$ fulfils all the group axioms $\text G 0$, $\text G 1$, $\text G 2$ and $\text G 3$.
Hence the result.
{{qed}}
Category:Finite Groups
tkm4fsduu4pixixo8kw4mgdmgehoooj
Theorem: Order Generating iff Every Superset Closed on Infima is Whole Space

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
{{iff}}
:$\forall Y \subseteq S: Y \supseteq X \land \paren {\forall Z \subseteq Y: \inf Z \in Y} \implies Y = S$

Proof:
=== Sufficient Condition ===
Let $X$ be order generating.
Let $Y \subseteq S$ such that
:$Y \supseteq X \land \paren {\forall Z \subseteq Y: \inf Z \in Y}$
We will prove that
:$S \subseteq Y$
Let $s \in S$.
By Order Generating iff Every Element is Infimum:
:$\exists Z \subseteq X: s = \inf Z$
By Subset Relation is Transitive:
:$Z \subseteq Y$
Thus by assumption:
:$s \in Y$
{{qed|lemma}}
By definition of set equality:
:$Y = S$
{{qed|lemma}}
Theorem: Group Isomorphism Preserves Inverses

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group isomorphism.
Let:
:$e_G$ be the identity of $\struct {G, \circ}$
:$e_H$ be the identity of $\struct {H, *}$.
Then:
: $\forall g \in G: \map \phi {g^{-1} } = \paren {\map \phi g}^{-1}$

Proof:
An group isomorphism is by definition a group epimorphism.
The result follows from Epimorphism Preserves Inverses.
{{Qed}}
Theorem: Group Isomorphism Preserves Inverses

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group isomorphism.
Let:
:$e_G$ be the identity of $\struct {G, \circ}$
:$e_H$ be the identity of $\struct {H, *}$.
Then:
: $\forall g \in G: \map \phi {g^{-1} } = \paren {\map \phi g}^{-1}$

Proof:
Let $g \in G$.
{{begin-eqn}}
{{eqn | l = \map \phi g * \map \phi {g^{-1} }
      | r = \map \phi {g \circ g^{-1} }
      | c = {{Defof|Group Isomorphism}}
}}
{{eqn | r = \map \phi {e_G}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = e_H
      | c = Group Isomorphism Preserves Identity
}}
{{end-eqn}}
It follows from Inverse in Group is Unique that $\map \phi {g^{-1} }$ is the unique inverse element of $\map \phi g$ in $\struct {H, *}$.
That is:
:$\forall g \in G: \map \phi {g^{-1} } = \paren {\map \phi g}^{-1}$
{{qed}}
Theorem: Preimage of Composite Relation

Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S_1 \times T_2$ be the composition of $\RR_1$ and $\RR_2$.
Then the preimage of $\RR_2 \circ \RR_1$ is given by:
:$\Preimg {\RR_2 \circ \RR_1} = \Preimg {\Img {\RR_1} \cap \Preimg {\RR_2} }$

Proof:
{{proof wanted}}
Category:Composite Relations
6lh1ebouq13pwncjkma96kpqrizpu1t
Theorem: Image of Composite Relation

Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S_1 \times T_2$ be the composition of $\RR_1$ and $\RR_2$.
Then the image of $\RR_2 \circ \RR_1$ is given by:
:$\Img {\RR_2 \circ \RR_1} = \Img {\Img {\RR_1} \cap \Preimg {\RR_2} }$

Proof:
We have by definition of composition of $\RR_1$ and $\RR_2$:
:$\RR_2 \circ \RR_1 := \set {\tuple {x, z} \in S_1 \times T_2: \exists y \in S_2 \cap T_1: \tuple {x, y} \in \RR_1 \land \tuple {y, z} \in \RR_2}$
Let $\left({x, z}\right) \in \RR_2 \circ \RR_1$.
By definition of image:
:$z \in \Img {\RR_2 \circ \RR_1}$
By definition of composition of $\RR_1$ and $\RR_2$:
:$z \in \Img {\RR_2}$
But also:
:$z \in \Img {\Img {\RR_1} }$
We also have that $\Img {\RR_2} = \Img {\Preimg {\RR_2} }$
That is:
$z \in \Img {\Img {\RR_1} } \cap \Img {\Preimg {\RR_2} }$
{{finish|Not convinced this is going to work.}}
Category:Composite Relations
b5ge9pk84j3e46bqba3xyq39i1lm3y0