avewright/proofwiki-math huggingface dataset:
Theorem: Composite of Epimorphisms is Epimorphism

Let:
:$\struct {S_1, \circ_1, \circ_2, \ldots, \circ_n}$
:$\struct {S_2, *_1, *_2, \ldots, *_n}$
:$\struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be algebraic structures.
Let:
:$\phi: \struct {S_1, \circ_1, \circ_2, \ldots, \circ_n} \to \struct {S_2, *_1, *_2, \ldots, *_n}$
:$\psi: \struct {S_2, *_1, *_2, \ldots, *_n} \to \struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be epimorphisms.
Then the composite of $\phi$ and $\psi$ is also an epimorphism.

Proof:
From Composite of Homomorphisms on Algebraic Structure is Homomorphism, $\psi \circ \phi$ is a homomorphism.
From Composite of Surjections is Surjection, $\psi \circ \phi$ is a surjection.
An epimorphism is a surjective homomorphism.
Hence $\psi \circ \phi$ is an epimorphism.
{{qed}}
Theorem: Composite of Automorphisms is Automorphism

Let $\struct {S, \odot_1, \odot_2, \ldots, \odot_n}$ be an algebraic structure.
Let:
:$\phi: \struct {S, \odot_1, \odot_2, \ldots, \odot_n} \to \struct {S, \odot_1, \odot_2, \ldots, \odot_n}$
:$\psi: \struct {S, \odot_1, \odot_2, \ldots, \odot_n} \to \struct {S, \odot_1, \odot_2, \ldots, \odot_n}$
be automorphisms.
Then the composite of $\phi$ and $\psi$ is also an automorphism.

Proof:
From Composite of Homomorphisms on Algebraic Structure is Homomorphism, $\psi \circ \phi$ is a homomorphism.
By the definition of a composite mapping, $\psi \circ \phi$ is a mapping from $S$ into $S$.
Hence $\psi \circ \phi$ is an automorphism.
{{qed}}
Theorem: Composite of Endomorphisms is Endomorphism

Let $\struct {S, \odot_1, \odot_2, \ldots, \odot_n}$ be an algebraic structure.
Let:
:$\phi: \struct {S, \odot_1, \odot_2, \ldots, \odot_n} \to \struct {S, \odot_1, \odot_2, \ldots, \odot_n}$
:$\psi: \struct {S, \odot_1, \odot_2, \ldots, \odot_n} \to \struct {S, \odot_1, \odot_2, \ldots, \odot_n}$
be endomorphisms.
Then the composite of $\phi$ and $\psi$ is also an endomorphism.

Proof:
From Composite of Homomorphisms on Algebraic Structure is Homomorphism, $\psi \circ \phi$ is a homomorphism.
From the definition of composition of mappings, $\psi \circ \phi$ is a mapping from $S$ into $S$.
Hence $\psi \circ \phi$ is an endomorphism.
{{qed}}
Theorem: Sine of Angle in Cartesian Plane

Let $P = \tuple {x, y}$ be a point in the cartesian plane whose origin is at $O$.
Let $\theta$ be the angle between the $x$-axis and the line $OP$.
Let $r$ be the length of $OP$.
Then:
:$\sin \theta = \dfrac y r$
where $\sin$ denotes the sine of $\theta$.

Proof:
:500px
Let a unit circle $C$ be drawn with its center at the origin $O$.
Let $Q$ be the point on $C$ which intersects $OP$.
$\angle OSP = \angle ORQ$, as both are right angles.
Both $\triangle OSP$ and $\triangle ORQ$ share angle $\theta$.
By Triangles with Two Equal Angles are Similar it follows that $\triangle OSP$ and $\triangle ORQ$ are similar.
By definition of similarity:
Then:
{{begin-eqn}}
{{eqn | l = \frac y r
      | r = \frac {SP} {OP}
      | c = 
}}
{{eqn | r = \frac {RQ} {OQ}
      | c = {{Defof|Similar Triangles}}
}}
{{eqn | r = RQ
      | c = $OP$ is Radius of Unit Circle
}}
{{eqn | r = \sin \theta
      | c = {{Defof|Sine|subdef = Definition from Circle}}
}}
{{end-eqn}}
When $\theta$ is obtuse, the same argument holds.
When $\theta = \dfrac \pi 2$ we have that $x = 0$.
Thus $y = r$ and $\sin \theta = 1 \dfrac y r$.
Thus the relation holds for $\theta = \dfrac \pi 2$.
When $\pi < \theta < 2 \pi$ the diagram can be reflected in the $x$-axis.
In this case, both $\sin \theta$ and $y$ are negative.
Thus the relation continues to hold.
When $\theta = 0$ and $\theta = \pi$ we have that $y = 0$ and $\sin \theta = 0 = \dfrac y r$.
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Sine of Angle

Let $\theta$ be an angle.
{{TFAE|def = Sine of Angle|view = sine of $\theta$}}

Proof:
=== Definition from Triangle implies Definition from Circle ===
Let $\sin \theta$ be defined as $\dfrac {\text{Opposite}} {\text{Hypotenuse}}$ in a right triangle.
Consider the triangle $\triangle OAP$.
By construction, $\angle OAP$ is a right angle.
Thus:
{{begin-eqn}}
{{eqn | l = \sin \theta
      | r = \frac {AP} {OP}
      | c = 
}}
{{eqn | r = \frac {AP} 1
      | c = as $OP$ is the radius of the unit circle
}}
{{eqn | r = AP
      | c = 
}}
{{end-eqn}}
That is:
: $\sin \theta = AP$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Cosine of Angle

Let $\theta$ be an angle.
{{TFAE|def = Cosine of Angle|view = cosine}}

Proof:
=== Definition from Triangle implies Definition from Circle ===
Let $\cos \theta$ be defined as $\dfrac {\text {Adjacent}} {\text {Hypotenuse}}$ in a right triangle.
Consider the triangle $\triangle OAP$.
By construction, $\angle OAP$ is a right angle.
From Parallelism implies Equal Alternate Angles:
:$\angle OPA = \theta$
Thus:
{{begin-eqn}}
{{eqn | l = \cos \theta
      | r = \frac {AP} {OP}
      | c = 
}}
{{eqn | r = \frac {AP} 1
      | c = as $OP$ is the radius of the unit circle
}}
{{eqn | r = AP
      | c = 
}}
{{end-eqn}}
That is:
:$\cos \theta = AP$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Tangent of Angle

Let $\theta$ be an angle.
{{TFAE|def = Tangent of Angle|view = Tangent of $\theta$}}

Proof:
=== Definition from Triangle implies Definition from Circle ===
Let $\tan \theta$ be defined as $\dfrac {\text{Opposite}} {\text{Adjacent}}$ in a right triangle.
Consider the triangle $\triangle OAB$.
By construction, $\angle OAB$ is a right angle.
Thus:
{{begin-eqn}}
{{eqn | l = \tan \theta
      | r = \frac {AB} {OA}
      | c = 
}}
{{eqn | r = \frac {AB} 1
      | c = as $OA$ is the radius of the unit circle
}}
{{eqn | r = AB
      | c = 
}}
{{end-eqn}}
That is:
: $\tan \theta = AB$
{{qed|lemma}}
Theorem: Cardinality of Subset Relation on Power Set of Finite Set

Let $S$ be a set such that:
:$\card S = n$
where $\card S$ denotes the cardinality of $S$.
From Subset Relation on Power Set is Partial Ordering we have that $\struct {\powerset S, \subseteq}$ is an ordered set.
The cardinality of $\subseteq$ as a relation is $3^n$.

Proof:
Let $X \in \powerset S$.
Since $X \subseteq S$, it follows that:
:$X' \subseteq X \implies X' \in \powerset S$
because the Subset Relation is Transitive.
From Cardinality of Power Set of Finite Set, it follows that for any $X \in \powerset S$:
:$\set {X' \in \powerset S: X' \subseteq X}$
has $2^{\card X}$ elements.
Therefore, the cardinality of $\subseteq$ is given by:
:$\ds \sum_{X \mathop \subseteq S} 2^{\card X}$
Let us split the sum over $\card X$:
:$\ds \sum_{X \mathop \subseteq S} 2^{\card X} = \sum_{k \mathop = 0}^n \sum_{\substack {X \mathop \subseteq S \\ \card X \mathop = n}} 2^{\card X}$
It now follows from Cardinality of Set of Subsets that:
:$\ds \card \subseteq = \sum_{k \mathop = 0}^n \binom n k 2^k$
From Binomial Theorem for Integral Index:
:$\ds \sum_{k \mathop = 0}^n \binom n k 2^k = \paren {1 + 2}^n$
Hence:
:$\card \subseteq = 3^n$
{{qed}}
Theorem: Quotient Structure of Semigroup is Semigroup

Let $\RR$ be a congruence relation on a semigroup $\struct {S, \circ}$.
Then the quotient structure $\struct {S / \RR, \circ_\RR}$ is a semigroup.

Proof:
From Quotient Structure is Well-Defined we have that $\circ_\RR$ is closed on $S / \RR$.
Let $\eqclass x \RR, \eqclass y \RR, \eqclass z \RR \in S / \RR$ under $\circ_\RR$ be arbitrary.
We shall prove that $\circ_\RR$ is associative:
{{begin-eqn}}
{{eqn | l = \paren {\eqclass x \RR \circ_\RR \eqclass y \RR} \circ_\RR \eqclass z \RR
      | r = \eqclass {x \circ y} \RR \circ_\RR \eqclass z \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass {\paren {x \circ y} \circ z} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass {x \circ \paren {y \circ z} } \RR
      | c = {{Semigroup-axiom|1}} under $\circ$
}}
{{eqn | r = \eqclass x \RR \circ_\RR \eqclass {y \circ z} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass x \RR \circ_\RR \paren {\eqclass y \RR \circ_\RR \eqclass z \RR}
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{end-eqn}}
Hence $\struct {S / \RR, \circ_\RR}$ is a semigroup.
{{qed}}
Theorem: Quotient Structure of Monoid is Monoid

Let $\RR$ be a congruence relation on a monoid $\struct {S, \circ}$ with an identity $e$.
Then the quotient structure $\struct {S / \RR, \circ_\RR}$ is a monoid.

Proof:
From Quotient Structure of Semigroup is Semigroup $\struct {S / \RR, \circ_\RR}$ is a semigroup.
Let $\eqclass x {\RR} \in S / \RR$.
Consider $\eqclass e \RR$:
{{begin-eqn}}
{{eqn | l = \eqclass x \RR \circ_\RR \eqclass e \RR
      | r = \eqclass {x \circ e} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass x \RR
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Furthermore:
{{begin-eqn}}
{{eqn | l = \eqclass e \RR \circ_\RR \eqclass x \RR
      | r = \eqclass {e \circ x} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass x \RR
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Hence $\eqclass e \RR$ is an identity.
Hence $\struct {S / \RR, \circ_\RR}$ is a monoid.
{{qed}}
Theorem: Quotient Structure of Group is Group

Let $\RR$ be a congruence relation on a group $\struct {G, \circ}$.
Then the quotient structure $\struct {G / \RR, \circ_\RR}$ is a group.

Proof:
From Quotient Structure of Monoid is Monoid $\struct {G / \RR, \circ_\RR}$ is a monoid with $\eqclass e \RR$ as its identity.
Let $\eqclass x \RR \in G / \RR$.
Let $x \in G$ be arbitrary.
Let $-x$ denote the inverse of $x \in G$ under $\circ$.
Consider the equivalence class $\eqclass {-x} \RR \in G / \RR$.
We need to show that:
{{begin-eqn}}
{{eqn | l = \eqclass x \RR \circ_{\RR} \eqclass {-x} \RR
      | r = \eqclass x \RR \circ_{\RR} \eqclass {-x} \RR
}}
{{eqn | r = \eqclass e \RR
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = \eqclass x \RR \circ_{\RR} \eqclass {-x} \RR
      | r = \eqclass {x \circ -x} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $G / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass e \RR
      | c = {{Defof|Inverse Element}} under $\circ$
}}
{{end-eqn}}
Furthermore:
{{begin-eqn}}
{{eqn | l = \eqclass {-x} \RR \circ_\RR \eqclass x \RR
      | r = \eqclass {-x \circ x} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $G / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass e \RR
      | c = {{Defof|Inverse Element}} under $\circ$
}}
{{end-eqn}}
Hence $\eqclass {-x} \RR$ is the inverse of $\eqclass x \RR$.
Hence $\struct {G / \RR, \circ_\RR}$ is a group.
{{qed}}
Theorem: Quotient Structure of Abelian Group is Abelian Group

Let $\RR$ be a congruence relation on an abelian group $\struct {G, \circ}$.
Then the quotient structure $\struct {G / \RR, \circ_\RR}$ is an abelian group.

Proof:
From Quotient Structure of Group is Group we have that $\struct {G / \RR, \circ_\RR}$ is a group.
Let $\eqclass x \RR, \eqclass y \RR \in S / \RR$.
{{begin-eqn}}
{{eqn | l = \eqclass x \RR \circ_\RR \eqclass y \RR
      | r = \eqclass {x \circ y} \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{eqn | r = \eqclass {y \circ x} \RR
      | c = $\circ$ is Commutative
}}
{{eqn | r = \eqclass y \RR \circ_\RR \eqclass x \RR
      | c = {{Defof|Operation Induced on Quotient Set|Operation Induced on $S / \RR$ by $\circ$}}
}}
{{end-eqn}}
Hence $\circ_\RR$ is commutative.
Hence $\struct {G / \RR, \circ_\RR}$ is an abelian group.
{{qed}}
Theorem: Quotient Structure is Similar to Structure

Let $\RR$ be a congruence relation on a algebraic structure $\struct {G, \circ}$.
{{MissingLinks|"similar" structure?}}
Then the quotient structure $\struct {G / \RR, \circ_\RR}$ is a similar structure to $\struct {G, \circ}$.

Proof:
=== Quotient Structure of Semigroup is Semigroup ===
{{:Quotient Structure of Semigroup is Semigroup}}
Theorem: Shape of Secant Function

The nature of the secant function on the set of real numbers $\R$ is as follows:
:$(1): \quad \sec x$ is continuous and strictly increasing on the intervals $\hointr 0 {\dfrac \pi 2}$ and $\hointl {\dfrac \pi 2} \pi$
:$(2): \quad \sec x$ is continuous and strictly decreasing on the intervals $\hointr {-\pi} {-\dfrac \pi 2}$ and $\hointl {-\dfrac \pi 2} 0$
:$(3): \quad \sec x \to + \infty$ as $x \to -\dfrac \pi 2^+$
:$(4): \quad \sec x \to + \infty$ as $x \to \dfrac \pi 2^-$
:$(5): \quad \sec x \to - \infty$ as $x \to \dfrac \pi 2^+$
:$(6): \quad \sec x \to - \infty$ as $x \to \dfrac {3 \pi} 2^-$

Proof:
From Derivative of Secant Function:
:$\map {D_x} {\sec x} = \dfrac {\sin x} {\cos^2 x}$
From Sine and Cosine are Periodic on Reals: Corollary:
:$\forall x \in \openint {-\pi} \pi \setminus \set {-\dfrac \pi 2, \dfrac \pi 2}: \cos x \ne 0$
Thus, from Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:
:$\forall x \in \openint {-\pi} \pi \setminus \set {-\dfrac \pi 2, \dfrac \pi 2}: \cos^2 x > 0$
{{improve|Might need to find a less abstract-algebraic version of the above result}}
From Sine and Cosine are Periodic on Reals: Corollary:
:$\sin x > 0$ on the open interval $\openint 0 \pi$
It follows that:
:$\forall x \in \openint 0 \pi \setminus \set {\dfrac \pi 2}: \dfrac {\sin x} {\cos^2 x} > 0$
From Sine and Cosine are Periodic on Reals: Corollary::
:$\sin x < 0$ on the open interval $\openint {-\pi} 0$
It follows that:
:$\forall x \in \openint {-\pi} 0 \setminus \set {-\dfrac \pi 2}: \dfrac {\sin x} {\cos^2 x} < 0$
Thus, $(1)$ and $(2)$ follow from Derivative of Monotone Function and Differentiable Function is Continuous.
From Zeroes of Sine and Cosine::
:$\cos - \dfrac \pi 2 = \cos \dfrac \pi 2 = \cos \dfrac {3 \pi} 2 = 0$
From Sine and Cosine are Periodic on Reals: Corollary:
:$\cos x > 0$ on the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$
From the same source:
:$\cos x < 0$ on the open interval $\openint {\dfrac \pi 2} {\dfrac {3 \pi} 2}$
Thus, $(3)$, $(4)$, $(5)$ and $(6)$ follow from Infinite Limit Theorem.
Theorem: Shape of Cosecant Function

The nature of the cosecant function on the set of real numbers $\R$ is as follows:
:$(1): \quad$ strictly decreasing on the intervals $\hointr {-\dfrac \pi 2} 0$ and $\hointl 0 {\dfrac \pi 2}$
:$(2): \quad$ strictly increasing on the intervals $\hointr {\dfrac \pi 2} \pi$ and $\hointl \pi {\dfrac {3 \pi} 2}$
:$(3): \quad$ $\csc x \to +\infty$ as $x \to 0^+$
:$(4): \quad$ $\csc x \to +\infty$ as $x \to \pi^-$
:$(5): \quad$ $\csc x \to -\infty$ as $x \to \pi^+$
:$(6): \quad$ $\csc x \to -\infty$ as $x \to 2 \pi^-$

Proof:
From Derivative of Cosecant Function::
:$\map {D_x} {\csc x} = -\dfrac {\cos x} {\sin^2 x}$
From Sine and Cosine are Periodic on Reals: Corollary:
:$\forall x \in \openint {-\dfrac \pi 2} {\dfrac {3 \pi} 2} \setminus \set {0, \pi}: \sin x \ne 0$
Thus, from Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:
:$\forall x \in \openint {-\dfrac \pi 2} {\dfrac {3 \pi} 2} \setminus \set {0, \pi}: \sin^2 x > 0$
{{improve|Might need to find a less abstract-algebraic version of the above result}}
From Sine and Cosine are Periodic on Reals: Corollary:
:$\cos x > 0$ on the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$
It follows that:
:$\forall x \in \openint {-\dfrac \pi 2} {\dfrac \pi 2} \setminus \set 0: -\dfrac {\cos x} {\sin^2 x} < 0$
From Sine and Cosine are Periodic on Reals: Corollary:
:$\cos x < 0$ on the open interval $\openint {\dfrac \pi 2} {\dfrac {3 \pi} 2}$
It follows that:
:$\forall x \in \openint {\dfrac \pi 2} {\dfrac {3 \pi} 2} \setminus \set \pi: -\dfrac {\cos x} {\sin^2 x} > 0$
Thus, $(1)$ and $(2)$ follow from Derivative of Monotone Function.
From Zeroes of Sine and Cosine: $\sin 0 = \sin \pi = \sin 2 \pi = 0$.
From Sine and Cosine are Periodic on Reals: Corollary:
:$\sin x > 0$ on the open interval $\openint 0 \pi$
From the same source:
:$\sin x < 0$ on the open interval $\openint \pi {2 \pi}$
Thus, $(3)$, $(4)$, $(5)$ and $(6)$ follow from Infinite Limit Theorem.
Theorem: Semigroup is Group Iff Latin Square Property Holds

Let $\struct {S, \circ}$ be a semigroup.
Then $\struct {S, \circ}$ is a group {{iff}} for all $a, b \in S$ the Latin square property holds in $S$:
:$a \circ x = b$
:$y \circ a = b$
for $x$ and $y$ each unique in $S$.

Proof:
=== Necessary Condition ===
Let $\struct {S, \circ}$ be a group.
$\struct {S, \circ}$ is a semigroup by the definition of a group.
By Group has Latin Square Property, the Latin square property holds in $S$.
{{qed|lemma}}
=== Sufficient Condition === 
Let $\struct {S, \circ}$ be a semigroup on which the Latin square property holds.
Taking the group axioms in turn:
==== {{Group-axiom|0}} ====
$\struct {S, \circ}$ is semigroup.
Hence $\struct {S, \circ}$ is closed by definition.
{{qed|lemma}}
==== {{Group-axiom|1}} ====
$\struct {S, \circ}$ is semigroup.
Hence $\circ$ is associative by definition.
{{qed|lemma}}
==== {{Group-axiom|2}} ====
Let $a \in S$.
Then there is an $x \in S$ such that:
{{begin-eqn}}
{{eqn | n = 1
      | l = a \circ x
      | r = a
}}
{{end-eqn}}
Let $b \in S$.
Then there is a $y \in S$ such that:
{{begin-eqn}}
{{eqn | n = 2
      | l = y \circ a
      | r = b
}}
{{end-eqn}}
Proving that $x$ is a right identity:
{{begin-eqn}}
{{eqn | l = b \circ x
      | r = \paren {y \circ a} \circ x
      | c = by $(2)$
}}
{{eqn | r = y \circ \paren {a \circ x}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = y \circ a
      | c = by $(1)$
}}
{{eqn | r = b
      | c = by $(2)$
}}
{{end-eqn}}
Let $c \in S$.
Then there is a $z \in S$ such that:
{{begin-eqn}}
{{eqn | n = 3
      | l = x \circ z
      | r = c
}}
{{end-eqn}}
Proving that $x$ is a left identity and thus an identity:
{{begin-eqn}}
{{eqn | l = x \circ c
      | r = x \circ \paren {x \circ z}
      | c = by $(3)$
}}
{{eqn | r = \paren {x \circ x} \circ z
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x \circ z
      | c = $x$ is a right identity
}}
{{eqn | r = c
      | c = by $(3)$
}}
{{end-eqn}}
Relabel $x$ as $e$.
{{qed|lemma}}
==== {{Group-axiom|3}} ====
Let $x \in S$.
Then $x$ has a right and left inverse by the property as there exists a $y$ and $z$ in $S$ such that:
{{begin-eqn}}
{{eqn | n = 4
      | l = x \circ y
      | r = e
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 5
      | l = z \circ x
      | r = e
}}
{{end-eqn}}
We shall prove that $y$ is also the left inverse of $x$:
{{begin-eqn}}
{{eqn | l = y \circ x
      | r = e \circ \paren {y \circ x}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {z \circ x} \circ \paren {y \circ x}
      | c = by $(5)$
}}
{{eqn | r = z \circ \paren {\paren {x \circ y} \circ x}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = z \circ \paren {e \circ x}
      | c = by $(4)$
}}
{{eqn | r = z \circ x
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = e
      | c = by $(5)$
}}
{{end-eqn}}
Hence every element of $S$ has a inverse.
{{qed}}
Theorem: Semigroup is Group Iff Latin Square Property Holds

Let $\struct {S, \circ}$ be a semigroup.
Then $\struct {S, \circ}$ is a group {{iff}} for all $a, b \in S$ the Latin square property holds in $S$:
:$a \circ x = b$
:$y \circ a = b$
for $x$ and $y$ each unique in $S$.

Proof:
=== Necessary Condition ===
Let $\struct {S, \circ}$ be a group.
$\struct {S, \circ}$ is a semigroup by the definition of a group.
By Group has Latin Square Property, the Latin square property holds in $S$.
{{qed|lemma}}
=== Sufficient Condition === 
Let $a \in G$.
We have {{hypothesis}}:
:$\exists e \in S: a \circ e = a$
and such an $e$ is unique.
Let $b \in G$.
Also {{hypothesis}}:
:$\exists x \in G: x \circ a = b$
and such an $x$ is unique.
Hence:
{{begin-eqn}}
{{eqn | l = b
      | r = x \circ a
      | c = 
}}
{{eqn | r = x \circ a \circ e
      | c = 
}}
{{eqn | r = b \circ e
      | c = 
}}
{{end-eqn}}
Also {{hypothesis}}:
:$\exists a' \in G: a' \circ a = e$
Thus $\struct {S, \circ}$ satisfies the right-hand Group Axioms
Thus $\struct {S, \circ}$ is a group.
{{qed}}
Theorem: Integer Multiples under Multiplication form Semigroup

Let $n \Z$ be the set of integer multiples of $n$.
Then $\struct {n \Z, \times}$ is a semigroup.
If $\size n > 1$ then $\struct {n \Z, \times}$ has no identity.

Proof:
=== Closure ===
Let $p, q \in n \Z$.
Then for some $p', q' \in \Z$:
:$p = n p'$
:$q = n q'$
Hence:
:$p q = \paren {n p'} \paren {n q'}$
By the commutativity and associativity of integer multiplication:
:$p q = n \paren {n \paren {p' q'} }$
Hence $p q \in n \Z$ and $n \Z$ is closed under $\times$.
{{qed|lemma}}
Theorem: Order of External Direct Product

Let $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ be algebraic structures.
Then the order of $\struct {S \times T, \circ}$ is $\card S \times \card T$.

Proof:
By definition the order of $\struct {S \times T, \circ}$ is $\card S \times \card T$ is the cardinality of the underlying set $S \times T$.
The result follows directly from Cardinality of Cartesian Product of Finite Sets.
{{qed}}
Theorem: Congruence (Number Theory) is Congruence Relation

Congruence modulo $m$ is a congruence relation on $\struct {\Z, +}$.

Proof:
Suppose $a \equiv b \bmod m$ and $c \equiv d \bmod m$.
Then by the definition of congruence there exists $k, k' \in \Z$ such that:
:$\paren {a - b} = k m$
:$\paren {c - d} = k' m$
Hence:
:$\paren {a - b} + \paren {c - d} = k m + k' m$
Using the properties of the integers:
:$\paren {a + c} - \paren {b + d} = m \paren {k + k'}$
Hence $\paren {a + c} \equiv \paren {b + d} \bmod m$ and congruence modulo $m$ is a congruence relation.
{{qed}}
Theorem: Group of Rationals Modulo One is Group

The set of equivalence classes $\Q / \Z$ with respect to the relation:
:$\forall a, b \in \Q: a \sim b \iff a - b \in \Z$
with the binary operation
:$\Q / \Z \times \Q / \Z \to \Q / \Z: \struct {\eqclass a {}, \eqclass b {} } \mapsto \eqclass {a + b} {}$
is an infinite abelian group.

Proof:
By Rational Numbers under Addition form Infinite Abelian Group, $\Q$ is an infinite Abelian group.
By Subgroup of Abelian Group is Normal, $\Z$ is a normal subgroup of $\Q$.
It follows from Quotient Group is Group that $\Q / \Z$ is a group.
By Quotient Group of Abelian Group is Abelian, $\Q / \Z$ is an Abelian group.
{{finish|It remains to be proven that $\Q / \Z$ is infinite}}
{{qed}}
Theorem: Rational Numbers with Denominators Coprime to Prime under Addition form Group

Let $p$ be a prime number.
Let $\Q_p$ denote the set:
:$\set {\dfrac r s : s \perp p}$
where $s \perp p$ denotes that $s$ is coprime to $p$.
Then $\struct {\Q_p, +}$ is a group.

Proof:
{{improve|For a neater proof, suggest the One-Step Subgroup Test or Two-Step Subgroup Test be used.}}
Taking each of the group axioms in turn:
Theorem: Equivalence of Definitions of Cotangent of Angle

Let $\theta$ be an angle.
{{TFAE|def = Cotangent of Angle|cotangent}}

Proof:
=== Definition from Triangle implies Definition from Circle ===
Let $\cot \theta$ be defined as $\dfrac {\text{Adjacent}} {\text{Opposite}}$ in a right triangle.
Consider the triangle $\triangle OAB$.
By construction, $\angle OAB$ is a right angle.
From Parallelism implies Equal Alternate Angles:
:$\angle OBA = \theta$
Thus:
{{begin-eqn}}
{{eqn | l = \cot \theta
      | r = \frac {AB} {OA}
      | c = 
}}
{{eqn | r = \frac {AB} 1
      | c = as $OA$ is the radius of the unit circle
}}
{{eqn | r = AB
      | c = 
}}
{{end-eqn}}
That is:
:$\cot \theta = AB$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Secant of Angle

Let $\theta$ be an angle.
{{TFAE|def = Secant of Angle|view = secant}}

Proof:
=== Definition from Triangle implies Definition from Circle ===
Let $\sec \theta$ be defined as $\dfrac {\text{Hypotenuse}} {\text{Adjacent}}$ in a right triangle.
Consider the triangle $\triangle OAB$.
By construction, $\angle OAB$ is a right angle.
Thus:
{{begin-eqn}}
{{eqn | l = \sec \theta
      | r = \frac {OB} {OA}
      | c = 
}}
{{eqn | r = \frac {OB} 1
      | c = as $OA$ is the radius of the unit circle
}}
{{eqn | r = OB
      | c = 
}}
{{end-eqn}}
That is:
: $\sec \theta = OB$
{{qed|lemma}}