avewright/proofwiki-math huggingface dataset:
Theorem: Intersection of Subgroups is Subgroup/General Result

Let $\mathbb S$ be a set of subgroups of $\struct {G, \circ}$, where $\mathbb S \ne \O$.
Then the intersection $\ds \bigcap \mathbb S$ of the elements of $\mathbb S$ is itself a subgroup of $G$.
Also, $\ds \bigcap \mathbb S$ is the largest subgroup of $\struct {G, \circ}$ contained in each element of $\mathbb S$.

Proof:
Let $\ds H = \bigcap \mathbb S$.
Let $H_k$ be an arbitrary element of $\mathbb S$.
Then:
{{begin-eqn}}
{{eqn | l = a, b
      | o = \in
      | r = H
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall k
      | l = a, b
      | o = \in
      | r = H_k
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadsto
      | q = \forall k
      | l = a \circ b^{-1}
      | o = \in
      | r = H_k
      | c = Group properties
}}
{{eqn | ll= \leadsto
      | l = a \circ b^{-1}
      | o = \in
      | r = H
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadsto
      | l = H
      | o = \le
      | r = G
      | c = One-Step Subgroup Test
}}
{{end-eqn}}
{{qed|lemma}}
Now to show that $\struct {H, \circ}$ is the largest such subgroup.
Let $K$ be a subgroup of $\struct {G, \circ}$ such that:
:$\forall S \in \mathbb S: K \subseteq S$
Then by definition $K \subseteq H$.
Let $x, y \in K$.
Then:
:$x \circ y^{-1} \in K \implies x \circ y^{-1} \in H$
Thus any subgroup of all elements of $\mathbb S$ is also a subgroup of $H$ and so no larger than $H$.
Thus $\ds H = \bigcap \mathbb S$ is the largest subgroup of $S$ contained in each element of $\mathbb S$.
{{qed}}
Theorem: Union of Subgroups/Corollary 2

Let $H \vee K$ be the join of $H$ and $K$.
Then $H \vee K = H \cup K$ {{iff}} $H \subseteq K$ or $K \subseteq H$.

Proof:
From the definition of join, $H \vee K$ is the smallest subgroup of $G$ containing $H \cup K$.
The result follows from Union of Subgroups.
{{qed}}
Theorem: Existence of Unique Subgroup Generated by Subset/Singleton Generator

Let $a \in G$.
Then $H = \gen a = \set {a^n: n \in \Z}$ is the unique smallest subgroup of $G$ such that $a \in H$.
That is:
: $K \le G: a \in K \implies H \subseteq K$

Proof:
From Powers of Element form Subgroup, $H = \set {a^n: n \in \Z}$ is a subgroup of $G$.
Let $K \le G: a \in K$.
Then $\forall n \in \Z: a^n \in K$.
Thus, $H \subseteq K$.
{{qed}}
Theorem: Intersection of Subsemigroups/General Result

Let $\mathbb H$ be a set of subsemigroups of $\struct {S, \circ}$, where $\mathbb H \ne \O$.
Then the intersection $\bigcap \mathbb H$ of the members of $\mathbb H$ is the largest subsemigroup of $\struct {S, \circ}$ contained in each member of $\mathbb H$.

Proof:
Let $T = \bigcap \mathbb S$.
Then:
{{begin-eqn}}
{{eqn | l = a, b
      | o = \in
      | r = T
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall K \in \mathbb S
      | l = a, b
      | o = \in
      | r = K
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | q = \forall K \in \mathbb S
      | l = a \circ b
      | o = \in
      | r = K
      | c = Subsemigroups are closed
}}
{{eqn | ll= \leadsto
      | l = a \circ b
      | o = \in
      | r = T
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
So by Subsemigroup Closure Test, $\struct {T, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Now to show that $\struct {T, \circ}$ is the largest such subsemigroup.
Let $x, y \in T$.
Then $\forall K \subseteq T: x \circ y \in K \implies x \circ y \in T$.
Thus $\forall K \in \mathbb S: K \subseteq T$.
Thus $T$ is the largest subsemigroup of $S$ contained in each member of $\mathbb S$.
{{qed}}
Theorem: Intersection of Subsemigroups/General Result

Let $\mathbb H$ be a set of subsemigroups of $\struct {S, \circ}$, where $\mathbb H \ne \O$.
Then the intersection $\bigcap \mathbb H$ of the members of $\mathbb H$ is the largest subsemigroup of $\struct {S, \circ}$ contained in each member of $\mathbb H$.

Proof:
From Set of Subsemigroups forms Complete Lattice:
:$\struct {\mathbb S, \subseteq}$ is a complete lattice.
where for every set $\mathbb H$ of subsemigroups of $S$:
:the infimum of $\mathbb H$ necessarily admitted by $\mathbb H$ is $\ds \bigcap \mathbb H$.
Hence the result, by definition of infimum.
{{qed}}
Theorem: Join of Subgroups is Group Generated by Union

Let $G$ be a group.
Let $H$ and $K$ be subgroups of $G$.
Let $S$ be the set of words of $H \cup K$.
Then $S$ is a subgroup of $K$ such that:
:$S = \gen {H \cup K} = H \vee K$
where $H \vee K$ denotes the join of $H$ and $K$.

Proof:
By definition, the set of words in $H \cup K$ is:
:$S = \map W {H \cup K} := \set {s_1 \circ s_2 \circ \cdots \circ s_n: n \in \N_{>0}: s_i \in H \cup K 1 \le i \le n}$
Let $h \in H$.
Then setting $n = 1$ in the above definition and letting $s_1 = h$ it follows that $H \subseteq S$.
Similarly it is seen that $K \subseteq S$
So from Union is Smallest Superset it follows that $H \cup K \subseteq S$.
From Set of Words Generates Group it follows that $S$ is the subgroup of $G$ generated by $H \cup K$.
{{qed}}
Theorem: Order of Subgroup Product/Corollary

:$\size {H \vee K} \ge \dfrac {\order H \order K} {\order {H \cap K} }$
or
:$\dfrac {\size {H \vee K} } {\order H} \ge \dfrac {\order K} {\order {H \cap K} }$
where $H \vee K$ denotes join and $\order H$ denotes the order of $H$.

Proof:
From Order of Subgroup Product:
: $(1): \quad \size {H K} = \dfrac {\order H \order K} {\order {H \cap K} }$
From Subset Product is Subset of Generator, we have that:
: $H K \subseteq H \vee K$
where $H K$ is the subset product of $H$ and $K$.
Thus:
: $(2): \quad \size {H \vee K} \ge \size {H K}$
The result follows by substituting for $\size {H K}$ from $(1)$ into $(2)$.
{{qed}}
Theorem: Abelian Group of Order Twice Odd has Exactly One Order 2 Element

Let $G$ be an abelian group whose identity element is $e$.
Let the order of $G$ be $2 n$ such that $n$ is odd.
Then there exists exactly one $g \in G$ with $g \ne e$ such that $g = g^{-1}$.

Proof:
By Even Order Group has Order 2 Element, $G$ has an element $x$ of order $2$.
{{AimForCont}} $y$ is another element of order $2$.
Then $x y = y x$ is another element of order $2$.
The subset $H = \set {g \in G: g^2 = e} = \set {e, x, y, x y}$ of $G$ forms a subgroup of $G$.
Thus $\order H = 4$.
But as $n$ is odd, it follows that $\order H$ is not a divisor of $2 n$.
This contradicts Lagrange's Theorem (Group Theory).
The result follows.
{{qed}}
Theorem: Homomorphic Image of Group Element is Coset

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Let $\map \ker \phi$ be the kernel of $\phi$.
Let $h \in H$.
Then $\Preimg h$ is either the empty set or a coset of $\map \ker \phi$.

Proof:
There are two possibilities for any $h \in H$.
:$(1): \quad \Preimg h = \O$
:$(2): \quad \Preimg h \ne \O$
If $(1)$, then the first disjunct of the result is satisfied.
Now suppose $(2)$ holds.
Let $e_G$ and $e_H$ be the identity elements of $G$ and $H$ respectively.
Let $K = \map \ker \phi$.
Let $x, y \in G$ such that $\map \phi x = \map \phi y$.
Then:
{{begin-eqn}}
{{eqn | l = e_H
      | r = \map \phi x * \paren {\map \phi y}^{-1}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = \map \phi x * \map \phi {y^{-1} }
      | c = Homomorphism to Group Preserves Inverses
}}
{{eqn | r = \map \phi {x \circ y^{-1} }
      | c = $\phi$ is a homomorphism
}}
{{eqn | ll= \leadsto
      | l = x \circ y^{-1}
      | o = \in
      | r = K
      | c = {{Defof|Kernel of Group Homomorphism}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = y K
      | c = Element in Left Coset iff Product with Inverse in Subgroup
}}
{{end-eqn}}
Thus:
:$\set {x: \map \phi x = \map \phi y}$ is a subset of $y K$.
From Kernel is Normal Subgroup of Domain we have that $y K = K y$.
Now suppose $x \in K y$.
Then, by definition, $x = k y$ for some $k \in K$.
Thus:
{{begin-eqn}}
{{eqn | l = x
      | r = k y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | r = \map \phi k * \map \phi y
      | c = $\phi$ is a homomorphism
}}
{{eqn | r = e_H * \map \phi y
      | c = {{Defof|Kernel of Group Homomorphism}}: $k \in K$
}}
{{eqn | r = \map \phi y
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
A similar process gives that $x \in y K \implies \map \phi x = \map \phi y$.
Hence the result.
{{qed}}
Theorem: Characterization of Metacategory via Equations

Let $\mathbf C_0$ and $\mathbf C_1$ be collections of objects.
Let $\operatorname{Cdm}$ and $\operatorname{Dom}$ assign to every element of $\mathbf C_1$ an element of $\mathbf C_0$.
Let $\operatorname{id}$ assign to every element of $\mathbf C_0$ an element of $\mathbf C_1$.
Denote with $\mathbf C_2$ the collection of pairs $\tuple {f, g}$ of elements of $\mathbf C_1$ satisfying:
:$\Dom g = \Cdm f$
Let $\circ$ assign to every such pair an element of $\mathbf C_1$.
Then $\mathbf C_0, \mathbf C_1, \operatorname{Cdm}, \operatorname{Dom}, \operatorname{id}$ and $\circ$ together determine a metacategory $\mathbf C$ {{iff}} the following seven axioms are satisfied:
{{begin-eqn}}
{{eqn | l = \Dom {\operatorname{id}_A} = A
      | o = \qquad
      | r = \Cdm {\operatorname{id}_A} = A
}}
{{eqn | l = f \circ \operatorname{id}_{\Dom f} = f
      | o = 
      | r = \operatorname{id}_{\Cdm f} \circ f = f
}}
{{eqn | l = \Dom {g \circ f} = \Dom f
      | o = 
      | r = \Cdm {g \circ f} = \Cdm g
}}
{{eqn | l = h \circ \paren {g \circ f}
      | r = \paren {h \circ g} \circ f
}}
{{end-eqn}}
where $A$ and $f, g, h$ are arbitrary elements of $\mathbf C_0$ and $\mathbf C_1$, respectively.
Further, in the last two lines, it is presumed that all compositions are defined.
{{refactor|extract into separate pages|level = medium}}
Hence it follows that:
* $\mathbf C_0$ and $\mathbf C_1$ represent the collections of objects and morphisms of $\mathbf C$
* $\operatorname{Dom}$ and $\operatorname{Cdm}$ represent the domain and codomain of a morphism of $\mathbf C$
* $\operatorname{id}$ represents the identity morphisms of $\mathbf C$
* $\mathbf C_2$ represents the collection of composable morphisms of $\mathbf C$
* $\circ$ represents the composition of morphisms in $\mathbf C$

Proof:
Let $\mathbf C_0$ and $\mathbf C_1$ be collections of objects.
Let $A$ in $C_O$ be arbitrary.
Let $f, g, h$ in $C_1$ be arbitrary.
By definition of identity morphism:
:$\Dom{\operatorname{id}_A} = \Cdm{\operatorname{id}_A} = A$
:$f \circ \operatorname{id}_A = f$
:$\operatorname{id}_A \circ g = g$
whenever $A$ is the domain of $f$ or the codomain of $g$, respectively.
From definition of identity morphism, since: 
:$\Dom{\operatorname{id}_A} = \Cdm{\operatorname{id}_A} = A$:
Therefore:
:$\Dom{\operatorname{id}_A} = A$
{{qed|lemma}}
Similarly, from definition of identity morphism, since: 
:$\Dom{\operatorname{id}_A} = \Cdm{\operatorname{id}_A} = A$:
Therefore:
:$\Cdm{\operatorname{id}_A} = A$
{{qed|lemma}}
From definition of identity morphism again, since:
:$f \circ \operatorname{id}_A = f$
and:
:$\Dom{\operatorname{id}_A} = A$
Therefore:
:$f \circ \operatorname{id}_A = f \circ \operatorname{id}_{\Dom f} $
Hence:
:$f \circ \operatorname{id}_{\Dom f} = f$
{{qed|lemma}}
From definition of identity morphism again, since:
:$\operatorname{id}_A \circ g = g$
and:
:$\Cdm{\operatorname{id}_A} = A$
Therefore:
:$\operatorname{id}_A \circ f = \operatorname{id}_{\Cdm f} \circ f $
Hence:
:$\operatorname{id}_{\Cdm f} \circ f = f$
{{qed|lemma}}
{{finish}}
Theorem: Kernel of Group Homomorphism Corresponds with Normal Subgroup of Domain

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Let $\map \ker \phi$ be the kernel of $\phi$.
Then there exists $N \lhd G$, a normal subgroup of $G$ such that:
:$N = \map \ker \phi$
Conversely, let $N \lhd G$ be normal subgroup of $G$.
Then there exists $\phi: \struct {G, \circ} \to \struct {H, *}$, a group homomorphism, whose kernel $\map \ker \phi$ is such that:
:$\map \ker \phi = N$

Proof:
The first statement is Kernel is Normal Subgroup of Domain:
:The kernel of $\phi$ is a normal subgroup of the domain of $\phi$:
::$\map \ker \phi \lhd \Dom \phi$
The second statement is Quotient Group Epimorphism is Epimorphism:
:The mapping $\phi: G \to G / N$, defined as:
::$\phi: G \to G / N: \map \phi x = x N$
:is a group epimorphism, and its kernel is $N$.
{{qed}}
Theorem: Inner Automorphism Maps Subgroup to Itself iff Normal

Let $G$ be a group.
For $x \in G$, let $\kappa_x$ denote the inner automorphism of $x$ in $G$.
Let $H$ be a subgroup of $G$.
Then:
:$\forall x \in G: \kappa_x \sqbrk H = H$
{{iff}}:
:$H$ is a normal subgroup of $G$.

Proof:
=== Sufficient Condition ===
{{:Inner Automorphism Maps Subgroup to Itself iff Normal/Sufficient Condition}}{{qed|lemma}}
Theorem: Group Epimorphism Preserves Normal Subgroups

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: G \to H$ be a group epimorphism.
Let $N \lhd G$, where $\lhd$ denotes that $N$ is a normal subgroup of $G$.
Then $\phi \sqbrk N \lhd H$.
That is, the image under $\phi$ of a normal subgroup is itself normal.

Proof:
Let $N' := \phi \sqbrk N$.
From Group Homomorphism Preserves Subgroups, $N'$ is a subgroup of $H$.
It remains to show that $N'$ is normal in $H$.
Let $h \in H$ be arbitrary.
Let $n' \in N'$ be arbitrary.
Because $\phi$ is an epimorphism, it is by definition surjective.
Therefore:
:$\exists n \in N: \map \phi n = n'$
:$\exists g \in G: \map \phi g = h$
Then:
{{begin-eqn}}
{{eqn | l = g \circ n \circ g^{-1}
      | o = \in
      | r = N
      | c = {{Defof|Normal Subgroup}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi {g \circ n \circ g^{-1} }
      | o = \in
      | r = N'
      | c = as $N'$ is the image of $N$
}}
{{eqn | ll= \leadsto
      | l = \map \phi g * \map \phi n * \map \phi {g^{-1} }
      | o = \in
      | r = N'
      | c = as $\phi$ has the morphism property
}}
{{eqn | ll= \leadsto
      | l = \map \phi g * \map \phi n * \paren {\map \phi g}^{-1}
      | o = \in
      | r = N'
      | c = Group Homomorphism Preserves Inverses
}}
{{eqn | ll= \leadsto
      | l = h * n' * h^{-1}
      | o = \in
      | r = N'
      | c = Definition of $g$ and $n$
}}
{{end-eqn}}
As $h$ and $n'$ were arbitrary, it follows that:
:$\forall h \in H, n' \in N': h * n' * h^{-1} \in N'$
and so $N'$ is a normal subgroup of $H$.
{{qed}}
Theorem: Group Epimorphism Induces Bijection between Subgroups

Let $G_1$ and $G_2$ be groups whose identities are $e_{G_1}$ and $e_{G_2}$ respectively.
Let $\phi: G_1 \to G_2$ be a group epimorphism.
Let $K := \map \ker \phi$ be the kernel of $\phi$.
Let $\mathbb H_1 = \set {H \subseteq G_1: H \le G_1, K \subseteq H}$ be the set of subgroups of $G_1$ which contain $K$.
Let $\mathbb H_2 = \set {H \subseteq G_2: H \le G_2}$ be the set of subgroups of $G_2$.
Then there exists a bijection $Q: \mathbb H_1 \leftrightarrow \mathbb H_2$ such that:
:$\forall N \lhd G_1: \map Q N \lhd G_2$
:$\forall N \lhd G_2: \map {Q^{-1} } N \lhd G_1$
where $N \lhd G_1$ denotes that $N$ is a normal subgroup of $G_1$.
That is, normal subgroups map bijectively to normal subgroups under $Q$.

Proof:
Let $Q$ be the mapping defined as:
:$\forall H \le \mathbb H_1: \map Q H = \set {\map \phi h: h \in H}$
Let $H$ be a subgroup of $G_1$ such that $K \subseteq H$.
From Group Homomorphism Preserves Subgroups, $\phi \sqbrk H$ is a subgroup of $G_2$.
This establishes that $Q$ is actually a mapping.
Let $N \lhd G_1$.
From Group Epimorphism Preserves Normal Subgroups, $\phi \sqbrk N$ is a normal subgroup of $G_2$.
This establishes that:
:$\forall N \lhd G_1: \map Q N \lhd G_2$
Next it is shown that $Q$ is a bijection.
Theorem: Group Epimorphism Induces Bijection between Subgroups/Corollary

Let $H \le G$ denote that $H$ is a subgroup of $G$.
Then:
:$\forall H \le G, K \subseteq H: \phi \sqbrk H \cong H / K$
where $H / K$ denotes the quotient group of $H$ by $K$.

Proof:
Let $H$ be a subgroup of $G$ such that $K \subseteq H$.
Consider the restriction of $\phi$ to $H$.
By Group Homomorphism Preserves Subgroups, $\phi_{\restriction_H} \sqbrk H$ is a group.
From Group Epimorphism Induces Bijection between Subgroups it follows that the First Isomorphism Theorem can be applied.
Hence the result.
{{qed}}
Theorem: Homomorphic Image of Quotient Group under Epimorphism

Let $G_1$ and $G_2$ be groups whose identities are $e_{G_1}$ and $e_{G_2}$ respectively.
Let $\phi: G_1 \to G_2$ be a group epimorphism.
Let $K := \map \ker \phi$ be the kernel of $\phi$.
Let $N$ be a normal subgroup of $G_1$ such that $K \subseteq N$.
Then:
:$\dfrac {G_1} N \cong \dfrac {G_2} {\map \phi N}$
where $\dfrac {G_1} N$ denotes the quotient group of $G_1$ by $N$.

Proof:
From Group Epimorphism Preserves Normal Subgroups, $\map \phi N$ is normal in $G_2$.
Let $N' := \map \phi N$.
From Quotient Group Epimorphism is Epimorphism, we construct the (group) epimorphism $q: G_2 \to \dfrac {G_2} {N'}$.
Now consider the composite mapping $q \circ \phi: G \to \dfrac {G_2} {N'}$ defined as:
:$\forall q \in G: \map {q \circ \phi} g = \map q {\map \phi g}$
From Composite of Group Epimorphisms is Epimorphism, $q \circ \phi$ is an epimorphism.
Let $g \in G$ such that:
:$\map {q \circ \phi} g = e_{G_2 / N'}$
where $e_{G_2 / N'}$ is the identity of $\dfrac {G_2} {N'}$.
Then $\map \phi g \in \map \ker q$.
But then by Group Epimorphism Induces Bijection between Subgroups it must be that $g \in N$.
Hence from the First Isomorphism Theorem, $\dfrac {G_2} {N'} \cong \dfrac {G_1} N$.
{{qed}}
Theorem: Cauchy's Group Theorem

Let $G$ be a finite group whose identity is $e$.
Let $p$ be a prime number which divides the order of $G$.
Then $G$ has a subgroup of order $p$.

Proof:
=== Lemma ===
Let $G$ be a finite abelian group whose identity is $e$.
Let $p$ be a prime number which divides the order of $G$.
Then $G$ has a subgroup of order $p$.
=== Proof of Lemma ===
Let $\order G$ be a prime number.
Then from Prime Group is Cyclic $G$ has a generator $\gen g$ such that $\order g = p$.
Now suppose $e \ne g \in G$.
Let $\order g = n$.
Let $p \divides n$.
Then by Subgroup of Finite Cyclic Group is Determined by Order the cyclic group $\gen g$ has an element $g$ of order $p$.
Suppose $p \nmid n$.
From Subgroup of Abelian Group is Normal, $\gen g$ is normal in $G$.
Consider the quotient group $G' = \dfrac G {\gen g}$.
As $p \nmid n$, $\gen e \subsetneq \gen g \subsetneq G$.
Thus $\order {G'} < \order G$.
But we have that $p \divides \order G$.
It follows by induction that $G'$ has an element $h'$ of order $p$.
Let $h$ be a preimage of $h'$ under the quotient epimorphism $\phi: G \to G'$.
Then:
:$\paren {h'}^p = e'$
where $e'$ is the identity of $G'$.
Thus $h^p \in \gen g$ so $\paren {h^p}^n = \paren {h^n}^p = e$.
Thus either $h^n$ has order $p$ or $h^n = e$.
If $h^n = e$ then $\paren {h'}^n = e'$.
But since $p$ is the order of $h'$ it would follow that $p \divides n$, contrary to assumption.
{{qed|lemma}}
{{tidy}}
{{MissingLinks}}
We prove the theorem by induction on the order $\order G$.
The first few cases $\order G = 1,2,3$ are obvious. For the induction step, start with the class equation
:$\order G = 1 + \order {C_2} + \cdots + \order {C_r}$
Since $p \divides \order G$, we must have $p \nmid \order {C_j}$ for some $j \geq 2$,
where $C_j$ are conjugacy classes in $G \setminus \set e$.
Let $x \in C_j$,
it follows that $p \divides \order {\map {C_G} x}$,
where $\map {C_G} x$ is the centralizer of $x$ in $G$,
since $\order {C_j} = \frac{\order G}{\order {\map {C_G} x}}$ by Number of Elements in Conjugacy Class Equals the Index of Centralizer.
If $\map {C_G} x \neq G$, then by induction $\map {C_G} x$ contains an element of order $p$, and this element also belongs to $G$.
Otherwise, $\map {C_G} x = G$, which implies that $x \in \map Z G$ (the center of $G$), and by choice $x \neq e$, so $\map Z G \neq \set e$.
Either $p \divides \order {\map Z G}$ or $p \nmid \order {\map Z G}$.
In the first case the proof reduces to lemma (the abelian case).
In the second case, by induction hypothesis to the quotient group $G / \map Z G$, there exists $x \in G$ such that the image $\bar{x} \in G / \map Z G$ has order $p$,
That is, $x^p \in \map Z G$ but $x \notin \map Z G$.
Let $X$ be the cyclic group generated by $x$.
Now the product $X \map Z G$ is abelian and has order divisible by $p$, so by lemma (the abelian case) it has an element of order $p$, and again this element also belongs to $G$.
This completes the induction step, and with it the proof.
{{qed}}
Theorem: Cauchy's Group Theorem

Let $G$ be a finite group whose identity is $e$.
Let $p$ be a prime number which divides the order of $G$.
Then $G$ has a subgroup of order $p$.

Proof:
This result follows as a special case of Group has Subgroups of All Prime Power Factors.
{{qed}}
Theorem: Metacategory Induces Morphisms-Only Metacategory

Let $\mathbf C$ be a metacategory.
Then the collection of morphisms $\mathbf C_1$ of $\mathbf C$ is a morphisms-only metacategory.

Proof:
In order to check that $\mathbf C_1$ is a morphisms-only metacategory, we need to interpret the symbols $\operatorname{dom}$, $\operatorname{cod}$ and $R_\circ$.
Set $\operatorname{dom} x := \operatorname{id}_{\operatorname{dom} x}$, and $\operatorname{cod} x := \operatorname{id}_{\operatorname{cod} x}$ with the symbols on the right as defined in $\mathbf C$.
Further, put $\map {R_\circ} {x, y, z} \iff x \circ y = z$.
Now we can proceed to verify the axioms for a morphisms-only metacategory.
For $(MOCT0)$, that is (omitting universal quantifiers):
:$\paren {\map {R_\circ} {x, y, z} \land \map {R_\circ} {x, y, z'} } \implies z = z'$
we conclude that the antecedent holds iff $z = x \circ y = z'$, hence $(MOCT0)$ holds.
{{qed|lemma}}
The content of $(MOCT1)$ is:
:$\operatorname{dom} x = \operatorname{cod} y \iff \exists z: \map {R_\circ} {x, y, z}$
This says that a composite morphism $x \circ y$ is defined {{iff}} $x$ and $y$ are composable morphisms.
{{qed|lemma}}
Axiom $(MOCT2)$ is the statement:
:$\map {R_\circ} {x, y, z} \implies \paren {\operatorname{dom} z = \operatorname{dom} y \land \operatorname{cod} z = \operatorname{cod} x}$
which prescribes the domain and codomain of $x \circ y$.
It follows directly from axiom $(C1)$ for metacategories that this is satisfied by $\mathbf C_1$.
{{qed|lemma}}
Axiom $(MOCT3)$ is:
:$\map {R_\circ} {x, y, a} \land \map {R_\circ} {y, z, b} \implies \paren {\exists w: \map {R_\circ} {x, b, w} \land \map{R_\circ} {a, z, w} }$
which expresses that $\circ$ is an associative operation, exactly as axiom $(C3)$ for metacategories specifies.
{{qed|lemma}}
Finally, axiom $(MOCT4)$ is the statement:
:$\map {R_\circ} {x, \operatorname{dom} x, x} \land \map {R_\circ} {\operatorname{cod} x, x, x}$
which will hold {{iff}}:
:$x \circ \operatorname{id}_{\operatorname{dom} x} = x$
and:
:$\operatorname{id}_{\operatorname{cod} x} \circ x = x$
This is the content of axiom $(C2)$ for metacategories.
{{qed|lemma}}
Having verified the axioms, we conclude $\mathbf C_1$ to be a morphisms-only metacategory.
{{qed}}