avewright/proofwiki-math huggingface dataset:
Theorem: Inverse of Product of Subsets of Group

Let $\struct {G, \circ}$ be a group.
Let $X, Y \subseteq G$.
Then:
:$\paren {X \circ Y}^{-1} = Y^{-1} \circ X^{-1}$
where $X^{-1}$ is the inverse of $X$.

Proof:
=== Superset ===
We will show that $\forall z \in Y^{-1} \circ X^{-1}: z \in \paren {X \circ Y}^{-1}$, from which:
:$Y^{-1} \circ X^{-1} \subseteq \paren {X \circ Y}^{-1}$
Let $z \in Y^{-1} \circ X^{-1}$.
By the definition of subset product:
:$\exists x' \in X^{-1}, y' \in Y^{-1}: z = y' \circ x'$
Then by Inverse of Group Product:
:$(2)\quad z^{-1} = x'^{-1} \circ y'^{-1}$
By the definition of inverse of subset:
:$x'^{-1} \in X$ and $y'^{-1} \in Y$
By the definition of subset product:
:$x'^{-1} \circ y'^{-1} \in X \circ Y$
Thus by $(2)$:
:$z^{-1} \in X \circ Y$
By the definition of inverse of subset:
:$z \in \paren {X \circ Y}^{-1}$
=== Subset ===
We will show that $\forall z \in \paren {X \circ Y}^{-1}: z \in Y^{-1} \circ X^{-1}$, from which:
:$\paren {X \circ Y}^{-1} \subseteq Y^{-1} \circ X^{-1}$
Let $z \in \paren {X \circ Y}^{-1}$.
By the definition of inverse of subset:
:$z^{-1} \in X \circ Y$
From Inverse of Inverse of Subset of Group:
:$z^{-1} \in \paren {X^{-1} }^{-1} \circ \paren {Y^{-1} }^{-1}$
Thus by the superset proof above:
:$z^{-1} \in \paren {Y^{-1} \circ X^{-1} }^{-1}$
From the definition of inverse of subset:
:$z \in Y^{-1} \circ X^{-1}$
{{qed}}
Theorem: Regular Representations in Group are Permutations

Let $\struct {G, \circ}$ be a group.
Let $a \in G$ be any element of $G$.
Then the left regular representation $\lambda_a$ and the right regular representation $\rho_a$ are permutations of $G$.

Proof:
This follows directly from the fact that all elements of a group are by definition invertible.
Therefore the result Regular Representation of Invertible Element is Permutation applies.
{{Qed}}
Theorem: Set Equivalence of Regular Representations

If $S$ is a finite subset of a group $G$, then:
:$\card {a \circ S} = \card S = \left|{S \circ a}\right|$
That is, $a \circ S$, $S$ and $S \circ a$ are equivalent: $a \circ S \sim S \sim S \circ a$.

Proof:
Follows immediately from the fact that both the left and right regular representation are permutations, and therefore bijections.
{{qed}}
Theorem: All Elements Self-Inverse then Abelian

Let $\struct {G, \circ}$ be a group.
Suppose that every element of $G$ is self-inverse.
Then $G$ is abelian.

Proof:
Every element of $G$ is self-inverse, that is:
:$\forall x \in G: x \circ x = e$
In particular, for all $x, y \in G$:
:$\paren {x \circ y} \circ \paren {x \circ y} = e$
that is, $x \circ y$ is also self-inverse.
From Self-Inverse Elements Commute iff Product is Self-Inverse, it follows that:
:$\forall x, y \in G: y \circ x = x \circ y$
that is: $x$ and $y$ commute for all $x, y \in G$.
Hence $G$ is an abelian group.
{{qed}}
Theorem: Commutation Property in Group

Let $\struct {G, \circ}$ be a group.
Then $x$ and $y$ commute {{iff}} $x \circ y \circ x^{-1} = y$.

Proof:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = y \circ x
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x \circ y} \circ x^{-1}
      | r = \paren {y \circ x} \circ x^{-1}
      | c = Cancellation Laws
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y \circ \paren {x \circ x^{-1} }
      | c = {{Defof|Associative Operation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y \circ e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ y \circ x^{-1}
      | r = y
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
{{qed}}
Theorem: Identity Mapping is Automorphism

The identity mapping $I_S: \struct {S, \circ} \to \struct {S, \circ}$ on the algebraic structure $\struct {S, \circ}$ is an automorphism.
Its image is $S$.

Proof:
By definition, an automorphism is an isomorphism from an algebraic structure onto itself.
An isomorphism, in turn, is a bijective homomorphism.
From Identity Mapping is Bijection, the identity mapping $I_S: S \to S$ on the set $S$ is a bijection from $S$ onto itself.
Now we need to show it is a homomorphism.
Let $x, y \in S$. Then:
{{begin-eqn}}
{{eqn | l = \map {I_S} {x \circ y}
      | r = x \circ y
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \map {I_S} x \circ \map {I_S} y
      | c = {{Defof|Identity Mapping}}
}}
{{end-eqn}}
Thus $\map {I_S} {x \circ y} = \map {I_S} x \circ \map {I_S} y$ and the morphism property holds/
This proves that $I_S: S \to S$ is a homomorphism.
As $I_S$ is a bijection, its image is $S$.
{{Qed}}
Theorem: Group Homomorphism of Product with Inverse

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x, y \in G
      | l = \map \phi {x \circ y^{-1} }
      | r = \map \phi x * \paren {\map \phi y}^{-1}
}}
{{eqn | n = 2
      | q = \forall x, y \in G
      | l = \map \phi {y^{-1} \circ x}
      | r = \paren {\map \phi y}^{-1} * \map \phi x
}}
{{end-eqn}}
where $y^{-1}$ denotes the inverse of $y$.

Proof:
Let $e_G$ and $e_H$ be the identities of $\struct {G, \circ}$ and $\struct {H, *}$ respectively.
By {{Group-axiom|0}}:
:$\forall x, y \in G: x \circ y^{-1} \in G, y^{-1} \circ x \in G$
;Result $(1)$:
{{begin-eqn}}
{{eqn | l = \map \phi {x \circ y^{-1} } * \map \phi y
      | r = \map \phi { \paren {x \circ y^{-1} } \circ y}
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \phi {x \circ \paren { y^{-1} \circ y} }
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \map \phi {x \circ e_G}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = \map \phi x
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\map \phi {x \circ y^{-1} } * \map \phi y} * \paren {\map \phi y}^{-1}
      | r = \map \phi x * \paren {\map \phi y}^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | l = \map \phi {x \circ y^{-1} } * \paren {\map \phi y * \paren {\map \phi y}^{-1} }
      | r = \map \phi x * \paren {\map \phi y}^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | l = \map \phi {x \circ y^{-1} } * e_H
      | r = \map \phi x * \paren {\map \phi y}^{-1}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | l = \map \phi {x \circ y^{-1} }
      | r = \map \phi x * \paren {\map \phi y}^{-1}
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
;Result $(2)$:
{{begin-eqn}}
{{eqn | l = \map \phi y * \map \phi {y^{-1} \circ x}
      | r = \map \phi {y \circ \paren {y^{-1} \circ x} }
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \phi {\paren {y \circ y^{-1} } \circ x }
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \map \phi {e_G \circ  x }
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = \map \phi x
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\map \phi y}^{-1} * \paren {\map \phi y * \map \phi {y^{-1} \circ x} }
      | r = \paren {\map \phi y}^{-1} * \map \phi x
      | c = {{Group-axiom|3}}
}}
{{eqn | l = \paren {\paren {\map \phi y}^{-1} * \map \phi y } * \map \phi {y^{-1} \circ x}
      | r = \paren {\map \phi y}^{-1} * \map \phi x
      | c = {{Group-axiom|1}}
}}
{{eqn | l = e_H * \map \phi {y^{-1} \circ x}
      | r = \paren {\map \phi y}^{-1} * \map \phi x
      | c = {{Defof|Inverse Element}}
}}
{{eqn | l = \map \phi {y^{-1} \circ x}
      | r = \paren {\map \phi y}^{-1} * \map \phi x
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mapping to Square is Endomorphism iff Abelian

Let $\struct {G, \circ}$ be a group.
Let $\phi: G \to G$ be defined as:
:$\forall g \in G: \map \phi g = g \circ g$
Then $\struct {G, \circ}$ is abelian {{iff}} $\phi$ is a (group) endomorphism.

Proof:
=== Necessary Condition ===
Let $\struct {G, \circ}$ be an abelian group.
Let $a, b \in G$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {a \circ b}
      | r = \paren {a \circ b} \circ \paren {a \circ b}
      | c = Definition of $\phi$
}}
{{eqn | r = a \circ \paren {b \circ a} \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | r = a \circ \paren {a \circ b} \circ b
      | c = {{Defof|Abelian Group}}: Commutativity
}}
{{eqn | r = \paren {a \circ a} \circ \paren {b \circ b}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \map \phi a \circ \map \phi b
      | c = Definition of $\phi$
}}
{{end-eqn}}
As $a$ and $b$ are arbitrary, the above holds for all $a, b \in G$.
Thus $\phi$ is a group homomorphism from $G$ to $G$.
So by definition, $\phi$ is a group endomorphism.
{{qed|lemma}}
Theorem: Induced Group Product is Homomorphism iff Commutative

Let $\struct {G, \circ}$ be a group.
Let $H_1, H_2$ be subgroups of $G$.
Let $\phi: H_1 \times H_2 \to G$ be defined such that:
:$\forall \tuple {h_1, h_2} \in H_1 \times H_2: \map \phi {h_1, h_2} = h_1 \circ h_2$
Then $\phi$ is a homomorphism {{iff}} every element of $H_1$ commutes with every element of $H_2$.

Proof:
We have $\tuple {h_1, h_2} \circ \tuple {k_1, k_2} = \tuple {h_1 \circ k_1, h_2 \circ k_2}$ by definition of group direct product.
Theorem: Isomorphism of Abelian Groups

Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group isomorphism.
Then $\struct {G, \circ}$ is abelian {{iff}} $\struct {H, *}$ is abelian.

Proof:
We have that Isomorphism Preserves Commutativity.
Thus:
:$\forall x, y \in G: x \circ y = y \circ x \implies \map \phi x * \map \phi y = \map \phi y * \map \phi x$
Thus if $G$ is abelian, so is $H$.
As $\phi^{-1}: H \to G$ is also an isomorphism, it is clear that if $H$ is abelian, then so is $G$.
{{qed}}
Theorem: Opposite Group is Group

Let $\struct {G, \circ}$ be a group.
Let $\struct {G, *}$ be the opposite group to $G$.
Then $\struct {G, *}$ is a group.

Proof:
=== {{Group-axiom|0|nolink}} ===
$\struct {G, *}$ is closed:
:$b \circ a \in G \implies a * b \in G$
{{qed|lemma}}
=== {{Group-axiom|1|nolink}} ===
$*$ is associative on $G$:
{{begin-eqn}}
{{eqn | l = a * \paren {b * c}
      | r = \paren {c \circ b} \circ a
      | c = Definition of $*$
}}
{{eqn | r = c \circ \paren {b \circ a}
      | c = Associativity of $\circ$
}}
{{eqn | r = \paren {a * b} * c
      | c = Definition of $*$
}}
{{end-eqn}}
{{qed|lemma}}
=== {{Group-axiom|2|nolink}} ===
Let $e$ be the identity of $\struct {G, \circ}$:
{{begin-eqn}}
{{eqn | l = a * e
      | r = e \circ a = a
}}
{{eqn | l = e * a
      | r = a \circ e = a
}}
{{end-eqn}}
Thus $e$ is the identity of $\struct {G, *}$.
{{qed|lemma}}
=== {{Group-axiom|3|nolink}} ===
Let the inverse of $a \in \struct {G, \circ}$ be $a^{-1}$:
{{begin-eqn}}
{{eqn | l = a * a^{-1}
      | r = a^{-1} \circ a = e
}}
{{eqn | l = a^{-1} * a
      | r = a \circ a^{-1} = e
}}
{{end-eqn}}
Thus $a^{-1}$ is the inverse of $a \in \struct {G, *}$
{{qed|lemma}}
So all the group axioms are satisfied, and $\struct {G, *}$ is a group.
{{qed}}
Theorem: Group Example: x inv c y

Let $\struct {G, \circ}$ be a group.
Let $c \in G$.
We define a new operation $*$ on $G$ as:
:$\forall x, y \in G: x * y = x \circ c^{-1} \circ y$
Then $\struct {G, *}$ is a group.

Proof:
=== {{Group-axiom|0|nolink}} ===
Let $x, y \in G$.
Then:
:$\forall x * y = x \circ c^{-1} \circ y \in G$ as $c^{-1} \in G$
thus demonstrating that $\struct {G, *}$ is closed.
{{qed|lemma}}
Theorem: Symmetric Difference on Power Set forms Abelian Group

Let $S$ be a set such that $\O \subset S$ (that is, $S$ is non-empty).
Let $A \symdif B$ be defined as the symmetric difference between $A$ and $B$.
Let $\powerset S$ denote the power set of $S$.
Then the algebraic structure $\struct {\powerset S, \symdif}$ is an abelian group.

Proof:
From Power Set is Closed under Symmetric Difference, we have that $\struct {\powerset S, \symdif}$ is closed.
The result follows directly from Set System Closed under Symmetric Difference is Abelian Group.
{{Qed}}
Theorem: Group is Subgroup of Itself

Let $\struct {G, \circ}$ be a group.
Then:
:$\struct {G, \circ} \le \struct {G, \circ}$
That is, a group is always a subgroup of itself.

Proof:
By Set is Subset of Itself, we have that:
:$G \subseteq G$
Thus $\struct {G, \circ}$ is a group which is a subset of $\struct {G, \circ}$, and therefore a subgroup of $\struct {G, \circ}$.
{{Qed}}
Theorem: Identity of Subgroup

Let $G$ be a group whose identity is $e$.
Let $H$ be a subgroup of group $G$.
Then the identity of $H$ is also $e$.

Proof:
A group is {{afortiori}} a monoid.
From the Cancellation Laws, all of its elements are cancellable.
The result then follows from Identity of Cancellable Monoid is Identity of Submonoid.
{{qed}}
Theorem: Inverses in Subgroup

Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Then for each $h \in H$, the inverse of $h$ in $H$ is the same as the inverse of $h$ in $G$.

Proof:
Let $h \in H$.
Let:
:$h'$ be the inverse of $h$ in $H$
:$h^{-1}$ be the inverse of $h$ in $G$.
From Identity of Subgroup:
:$h \circ h' = e$
From Inverse in Group is Unique, it follows that $h' = h^{-1}$.
{{qed}}
Theorem: Subgroup of Abelian Group is Abelian

A subgroup of an abelian group is itself abelian.

Proof:
Follows directly from Restriction of Commutative Operation is Commutative.
{{qed}}
Theorem: Intersection of Subgroups is Subgroup

The intersection of two subgroups of a group is itself a subgroup of that group:
:$\forall H_1, H_2 \le \struct {G, \circ}: H_1 \cap H_2 \le G$
It also follows that $H_1 \cap H_2 \le H_1$ and $H_1 \cap H_2 \le H_2$.

Proof:
Let $H = H_1 \cap H_2$ where $H_1, H_2 \le \struct {G, \circ}$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = a, b \in H
      | c = 
}}
{{eqn | o = \leadsto
      | r = a, b \in H_1 \land a, b \in H_2
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = a \circ b^{-1} \in H_1 \land a \circ b^{-1} \in H_2
      | c = Group Properties
}}
{{eqn | o = \leadsto
      | r = a \circ b^{-1} \in H
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = H \le G
      | c = One-Step Subgroup Test
}}
{{end-eqn}}
As $H \subseteq H_1$ and $H \subseteq H_2$, the other results follow directly.
{{qed}}
Theorem: Union of Subgroups

Let $\struct {G, \circ}$ be a group.
Let $H, K \le G$ be subgroups of $G$.
Let neither $H \subseteq K$ nor $K \subseteq H$.
Then $H \cup K$ is ''not'' a subgroup of $G$.

Proof:
As neither $H \subseteq K$ nor $K \subseteq H$, it follows from Set Difference with Superset is Empty Set that neither $H \setminus K = \O$ nor $K \setminus H = \O$.
So, let $h \in H \setminus K, k \in K \setminus H$.
Thus, $h \notin K, k \notin H$.
If $\struct {H \cup K, \circ}$ is a group, then it must be closed.
If $\struct {H \cup K, \circ}$ is closed, then $h \circ k \in H \cup K \implies h \circ k \in H \lor h \circ k \in K$.
If $h \circ k \in H$ then $h^{-1} \circ h \circ k \in H \implies k \in H$.
If $h \circ k \in K$ then $h \circ k \circ k^{-1} \in K \implies h \in K$.
So $h \circ k$ can be in neither $H$ nor $K$.
Therefore $\struct {H \cup K, \circ}$ is not closed.
Therefore $H \cup K$ is not a subgroup of $G$.
{{qed}}
Theorem: Elements of Group with Equal Images under Homomorphisms form Subgroup

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $f: G \to H$ and $g: G \to H$ be group homomorphisms.
Then the set:
:$S = \set {x \in G: \map f x = \map g x}$
is a subgroup of $G$.

Proof:
Let the identities of $\struct {G, \circ}$ and $\struct {H, *}$ be $e_G$ and $e_H$ respectively.
By Homomorphism to Group Preserves Identity:
:$\map f {e_G} = \map g {e_G} = e_H$
Thus $e_G \in S$, and so $S \ne \O$.
Similarly, from Homomorphism to Group Preserves Inverses, $x \in S \implies x^{-1} \in S$.
Let $x, y \in S$. Then:
{{begin-eqn}}
{{eqn | l = \map f {x \circ y}
      | r = \map f x * \map f y
      | c = Morphism Property
}}
{{eqn | r = \map g x * \map g y
      | c = Definition of $S$
}}
{{eqn | r = \map g {x \circ y}
      | c = Morphism Property
}}
{{end-eqn}}
Thus $x \circ y \in S$.
So, by the Two-Step Subgroup Test:
:$S \le G$
{{Qed}}
Theorem: Product of Subgroup with Itself

Let $\struct {G, \circ}$ be a group.
Then:
:$\forall H \le G: H \circ H = H$
where:
:$H \circ H$ denotes the subset product of $H$ with $H$
:$\le$ denotes the subgroup relation.

Proof:
From Magma Subset Product with Self, we have:
:$H \circ H \subseteq H$
Let $e$ be the identity of $G$.
By Identity of Subgroup, it is also the identity of $H$.
So:
{{begin-eqn}}
{{eqn | l = h
      | o = \in
      | r = H
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e \circ h
      | o = \in
      | r = H \circ H
      | c = 
}}
{{eqn | ll= \leadsto
      | l = h
      | o = \in
      | r = H \circ H
      | c = 
}}
{{eqn | ll= \leadsto
      | l = H
      | o = \subseteq
      | r = H \circ H
      | c = 
}}
{{end-eqn}}
Hence the result from the definition of set equality.
{{qed}}
Theorem: Inverse of Subgroup

Let $\struct {G, \circ}$ be a group.
Let $H$ be a subgroup of $G$.
Then:
:$H^{-1} = H$
where $H^{-1}$ is the inverse of $H$.

Proof:
As $H$ is a subgroup of $G$:
:$\forall h \in H: h^{-1} \in H$
The result follows.
{{qed}}
Theorem: Subset Product of Subgroups

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Then $H \circ K$ is a subgroup of $G$ {{iff}} $H$ and $K$ are permutable.
That is:
$H \circ K$ is a subgroup of $G$ {{iff}}:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K$ is a subgroup of $G$.
Let $h \circ k \in H \circ K$.
Then $h \circ k$ is the inverse of some element $g$ of $H \circ K$.
Thus we can write $g = h' \circ k'$ for some $h' \in H$ and $k' \in K$.
So:
{{begin-eqn}}
{{eqn | l = h \circ k
      | r = g^{-1}
      | c = Inverse of Group Inverse: $g$ is the inverse of $h \circ k$
}}
{{eqn | r = \paren {h' \circ k'}^{-1}
      | c = 
}}
{{eqn | r = k'^{-1} \circ h'^{-1}
      | c = Inverse of Group Product
}}
{{eqn | o = \in
      | r = K \circ H
      | c = as $K$ and $H$ are both groups
}}
{{end-eqn}}
So by definition of subset:
: $H \circ K \subseteq K \circ H$
Now suppose $x \in K \circ H$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = k \circ h
      | c = for some $k \in K, h \in H$
}}
{{eqn | r = \paren {\paren {k \circ h}^{-1} }^{-1}
      | c = Inverse of Group Inverse
}}
{{eqn | r = \paren {h^{-1} \circ k^{-1} }^{-1}
      | c = Inverse of Group Product
}}
{{eqn | o = \in
      | r = H \circ K
      | c = as $K$ and $H$ are both groups
}}
{{end-eqn}}
So by definition of subset:
:$K \circ H \subseteq H \circ K$
The result follows by definition of set equality.
{{qed}}
Theorem: Subset Product of Subgroups

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Then $H \circ K$ is a subgroup of $G$ {{iff}} $H$ and $K$ are permutable.
That is:
$H \circ K$ is a subgroup of $G$ {{iff}}:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K$ is a subgroup of $G$.
Then:
{{begin-eqn}}
{{eqn | l = H \circ K
      | r = \paren {H \circ K}^{-1}
      | c = Inverse of Subgroup
}}
{{eqn | r = K^{-1} \circ H^{-1}
      | c = Inverse of Product of Subsets of Group
}}
{{eqn | r = K \circ H
      | c = Inverse of Subgroup
}}
{{end-eqn}}
{{qed}}
Theorem: Subset Product of Subgroups

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Then $H \circ K$ is a subgroup of $G$ {{iff}} $H$ and $K$ are permutable.
That is:
$H \circ K$ is a subgroup of $G$ {{iff}}:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K = K \circ H$.
First note that $H \circ K \ne \O$, as $e_G = e_G \circ e_G \in H \circ K$, from Identity of Subgroup.
Suppose $a_1, a_2 \in H, b_1, b_2 \in K$.
Then:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} = a_1 \circ \paren {b_1 \circ a_2} \circ b_2$.
Since $H \circ K = K \circ H$, we see that, for some $a \in H, b \in K$:
:$b_1 \circ a_2 = a \circ b$
Thus:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} = \paren {a_1 \circ a} \circ \paren {b \circ b_2}$
As $H, K \le G$, we have $a_1 \circ a \in H$ and $b \circ b_2 \in K$, hence:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} \in H \circ K$
thus demonstrating closure of $H \circ K$ under $\circ$.
Finally, if $a \circ b \in H \circ K$, then by Inverse of Group Product:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$
Since $b^{-1} \in K$ and $a^{-1} \in H$, we have:
:$\paren {a \circ b}^{-1} \in K \circ H$
and hence $H \circ K$ is shown to be closed under inverses.
Thus, from the Two-Step Subgroup Test, $H \circ K$ is a subgroup of $G$.
{{qed}}
Theorem: Subset Product of Subgroups

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Then $H \circ K$ is a subgroup of $G$ {{iff}} $H$ and $K$ are permutable.
That is:
$H \circ K$ is a subgroup of $G$ {{iff}}:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K = K \circ H$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {H \circ K} \circ \paren {H \circ K}^{-1}
      | r = H \circ K \circ K^{-1} \circ H^{-1}
      | c = Inverse of Product of Subsets of Group
}}
{{eqn | r = H \circ K \circ K \circ H
      | c = Inverse of Subgroup
}}
{{eqn | r = H \circ K \circ H
      | c = Product of Subgroup with Itself
}}
{{eqn | r = H \circ H \circ K
      | c = by hypothesis
}}
{{eqn | r = H \circ K
      | c = Product of Subgroup with Itself
}}
{{end-eqn}}
That is:
:$\paren {H \circ K} \circ \paren {H \circ K}^{-1} = H \circ K$
Thus by definition of set equality:
:$\paren {H \circ K} \circ \paren {H \circ K}^{-1} \subseteq H \circ K$
So from One-Step Subgroup Test using Subset Product:
:$H \circ K \le G$
{{qed}}
Theorem: Group Homomorphism Preserves Subgroups

Let $\struct {G_1, \circ}$ and $\struct {G_2, *}$ be groups.
Let $\phi: \struct {G_1, \circ} \to \struct {G_2, *}$ be a group homomorphism. 
Then:
:$H \le G_1 \implies \phi \sqbrk H \le G_2$
where:
:$\phi \sqbrk H$ denotes the image of $H$ under $\phi$
:$\le$ denotes subgroup.
That is, group homomorphism preserves subgroups.

Proof:
Let $H \le G_1$.
First note that from Null Relation is Mapping iff Domain is Empty Set:
:$H \ne \O \implies \phi \sqbrk H \ne \O$
and so $\phi \sqbrk H$ is not empty.
Next, let $x, y \in \phi \sqbrk H$.
Then:
:$\exists h_1, h_2 \in H: x = \map \phi {h_1}, y = \map \phi {h_2}$
From the definition of Group Homomorphism, we have:
:$\map \phi {h_1^{-1} \circ h_2} = x^{-1} * y$
Since $H$ is a subgroup:
:$h_1^{-1} \circ h_2 \in H$
Hence:
:$x^{-1} * y \in \phi \sqbrk H$
Thus from the One-Step Subgroup Test:
:$\phi \sqbrk H \le G_2$
{{qed}}
Theorem: Image of Group Homomorphism is Subgroup

Let $\phi: G_1 \to G_2$ be a group homomorphism.
Then:
:$\Img \phi \le G_2$
where $\le$ denotes the relation of being a subgroup.

Proof:
This is a special case of Group Homomorphism Preserves Subgroups, where we set $H = G_1$.
{{Qed}}
Theorem: Conjugacy is Equivalence Relation

Conjugacy of group elements is an equivalence relation.

Proof:
Checking each of the criteria for an equivalence relation in turn:
Theorem: Kernel of Group Homomorphism is Subgroup

The kernel of a group homomorphism is a subgroup of its domain:
:$\map \ker \phi \le \Dom \phi$

Proof:
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
From Homomorphism to Group Preserves Identity, $\map \phi {e_G} = e_H$, so $e_G \in \map \ker \phi$.
Therefore $\map \ker \phi \ne \O$.
Let $x, y \in \map \ker \phi$, so that $\map \phi x = \map \phi y = e_H$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {x^{-1} \circ y}
      | r = \map \phi {x^{-1} } * \map \phi y
      | c = {{Defof|Morphism Property}}
}}
{{eqn | r = \paren {\map \phi x}^{-1} * \map \phi y
      | c = Homomorphism with Identity Preserves Inverses
}}
{{eqn | r = e_H^{-1} * e_H
      | c = as $x, y \in \map \ker \phi$
}}
{{eqn | r = e_H
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
So $x^{-1} \circ y \in \map \ker \phi$, and from the One-Step Subgroup Test, $\map \ker \phi \le \Dom \phi$.
{{qed}}